Intervals in ℕ as finsets
For now this only covers Ico n m, the "closed-open" interval containing [n, ..., m-1].
intervals
Ico n m is the set of natural numbers n ≤ k < m.
Equations
- finset.Ico n m = {val := multiset.Ico n m, nodup := _}
@[simp]
theorem
finset.Ico.image_add
(n m k : ℕ) :
finset.image (has_add.add k) (finset.Ico n m) = finset.Ico (n + k) (m + k)
theorem
finset.Ico.image_sub
(n m k : ℕ) :
k ≤ n → finset.image (λ (x : ℕ), x - k) (finset.Ico n m) = finset.Ico (n - k) (m - k)
theorem
finset.Ico.subset_iff
{m₁ n₁ m₂ n₂ : ℕ} :
m₁ < n₁ → (finset.Ico m₁ n₁ ⊆ finset.Ico m₂ n₂ ↔ m₂ ≤ m₁ ∧ n₁ ≤ n₂)
theorem
finset.Ico.subset
{m₁ n₁ m₂ n₂ : ℕ} :
m₂ ≤ m₁ → n₁ ≤ n₂ → finset.Ico m₁ n₁ ⊆ finset.Ico m₂ n₂
theorem
finset.Ico.union_consecutive
{n m l : ℕ} :
n ≤ m → m ≤ l → finset.Ico n m ∪ finset.Ico m l = finset.Ico n l
@[simp]
theorem
finset.Ico.succ_top
{n m : ℕ} :
n ≤ m → finset.Ico n (m + 1) = has_insert.insert m (finset.Ico n m)
theorem
finset.Ico.succ_top'
{n m : ℕ} :
n < m → finset.Ico n m = has_insert.insert (m - 1) (finset.Ico n (m - 1))
theorem
finset.Ico.insert_succ_bot
{n m : ℕ} :
n < m → has_insert.insert n (finset.Ico (n + 1) m) = finset.Ico n m
theorem
finset.Ico.filter_lt_of_top_le
{n m l : ℕ} :
m ≤ l → finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = finset.Ico n m
theorem
finset.Ico.filter_lt_of_le_bot
{n m l : ℕ} :
l ≤ n → finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = ∅
theorem
finset.Ico.filter_Ico_bot
{n m : ℕ} :
n < m → finset.filter (λ (x : ℕ), x ≤ n) (finset.Ico n m) = {n}
theorem
finset.Ico.filter_lt_of_ge
{n m l : ℕ} :
l ≤ m → finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = finset.Ico n l
@[simp]
theorem
finset.Ico.filter_lt
(n m l : ℕ) :
finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = finset.Ico n (min m l)
theorem
finset.Ico.filter_le_of_le_bot
{n m l : ℕ} :
l ≤ n → finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = finset.Ico n m
theorem
finset.Ico.filter_le_of_top_le
{n m l : ℕ} :
m ≤ l → finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = ∅
theorem
finset.Ico.filter_le_of_le
{n m l : ℕ} :
n ≤ l → finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = finset.Ico l m
@[simp]
theorem
finset.Ico.filter_le
(n m l : ℕ) :
finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = finset.Ico (max n l) m
@[simp]
theorem
finset.Ico.diff_left
(l n m : ℕ) :
finset.Ico n m \ finset.Ico n l = finset.Ico (max n l) m
@[simp]
theorem
finset.Ico.diff_right
(l n m : ℕ) :
finset.Ico n m \ finset.Ico l m = finset.Ico n (min m l)
theorem
finset.Ico.image_const_sub
{k m n : ℕ} :
k ≤ n → finset.image (λ (j : ℕ), n - j) (finset.Ico k m) = finset.Ico (n + 1 - m) (n + 1 - k)
theorem
finset.range_image_pred_top_sub
(n : ℕ) :
finset.image (λ (j : ℕ), n - 1 - j) (finset.range n) = finset.range n
Ico_ℤ l u is the set of integers l ≤ k < u.
Equations
- finset.Ico_ℤ l u = finset.map {to_fun := λ (n : ℕ), ↑n + l, inj' := _} (finset.range (u - l).to_nat)