mathlib documentation

data.finset.intervals

Intervals in ℕ as finsets

For now this only covers Ico n m, the "closed-open" interval containing [n, ..., m-1].

intervals

source
def finset.Ico (n m : ℕ) :
finset ℕ

Ico n m is the set of natural numbers n ≤ k < m.

Equations
source
@[simp]
theorem finset.Ico.val (n m : ℕ) :
(finset.Ico n m).val = multiset.Ico n m

source
@[simp]
theorem finset.Ico.to_finset (n m : ℕ) :
(multiset.Ico n m).to_finset = finset.Ico n m

source
theorem finset.Ico.image_add (n m k : ℕ) :
finset.image (has_add.add k) (finset.Ico n m) = finset.Ico (n + k) (m + k)

source
theorem finset.Ico.image_sub (n m k : ℕ) (h : k ≤ n) :
finset.image (λ (x : ℕ), x - k) (finset.Ico n m) = finset.Ico (n - k) (m - k)

source
theorem finset.Ico.zero_bot (n : ℕ) :
finset.Ico 0 n = finset.range n

source
@[simp]
theorem finset.Ico.card (n m : ℕ) :
(finset.Ico n m).card = m - n

source
@[simp]
theorem finset.Ico.mem {n m l : ℕ} :
l ∈ finset.Ico n m ↔ n ≤ l ∧ l < m

source
theorem finset.Ico.eq_empty_of_le {n m : ℕ} (h : m ≤ n) :
finset.Ico n m = ∅

source
@[simp]
theorem finset.Ico.self_eq_empty (n : ℕ) :
finset.Ico n n = ∅

source
@[simp]
theorem finset.Ico.eq_empty_iff {n m : ℕ} :
finset.Ico n m = ∅ ↔ m ≤ n

source
theorem finset.Ico.subset_iff {m₁ n₁ m₂ n₂ : ℕ} (hmn : m₁ < n₁) :
finset.Ico m₁ n₁ ⊆ finset.Ico m₂ n₂ ↔ m₂ ≤ m₁ ∧ n₁ ≤ n₂

source
theorem finset.Ico.subset {m₁ n₁ m₂ n₂ : ℕ} (hmm : m₂ ≤ m₁) (hnn : n₁ ≤ n₂) :
finset.Ico m₁ n₁ ⊆ finset.Ico m₂ n₂

source
theorem finset.Ico.union_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) :
finset.Ico n m ∪ finset.Ico m l = finset.Ico n l

source
@[simp]
theorem finset.Ico.inter_consecutive (n m l : ℕ) :
finset.Ico n m ∩ finset.Ico m l = ∅

source
theorem finset.Ico.disjoint_consecutive (n m l : ℕ) :
disjoint (finset.Ico n m) (finset.Ico m l)

source
@[simp]
theorem finset.Ico.succ_singleton (n : ℕ) :
finset.Ico n (n + 1) = {n}

source
theorem finset.Ico.succ_top {n m : ℕ} (h : n ≤ m) :
finset.Ico n (m + 1) = insert m (finset.Ico n m)

source
theorem finset.Ico.succ_top' {n m : ℕ} (h : n < m) :
finset.Ico n m = insert (m - 1) (finset.Ico n (m - 1))

source
theorem finset.Ico.insert_succ_bot {n m : ℕ} (h : n < m) :
insert n (finset.Ico (n + 1) m) = finset.Ico n m

source
@[simp]
theorem finset.Ico.pred_singleton {m : ℕ} (h : 0 < m) :
finset.Ico (m - 1) m = {m - 1}

source
@[simp]
theorem finset.Ico.not_mem_top {n m : ℕ} :
m ∉ finset.Ico n m

source
theorem finset.Ico.filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) :
finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = finset.Ico n m

source
theorem finset.Ico.filter_lt_of_le_bot {n m l : ℕ} (hln : l ≤ n) :
finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = ∅

source
theorem finset.Ico.filter_Ico_bot {n m : ℕ} (hnm : n < m) :
finset.filter (λ (x : ℕ), x ≤ n) (finset.Ico n m) = {n}

source
theorem finset.Ico.filter_lt_of_ge {n m l : ℕ} (hlm : l ≤ m) :
finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = finset.Ico n l

source
@[simp]
theorem finset.Ico.filter_lt (n m l : ℕ) :
finset.filter (λ (x : ℕ), x < l) (finset.Ico n m) = finset.Ico n (min m l)

source
theorem finset.Ico.filter_le_of_le_bot {n m l : ℕ} (hln : l ≤ n) :
finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = finset.Ico n m

source
theorem finset.Ico.filter_le_of_top_le {n m l : ℕ} (hml : m ≤ l) :
finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = ∅

source
theorem finset.Ico.filter_le_of_le {n m l : ℕ} (hnl : n ≤ l) :
finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = finset.Ico l m

source
@[simp]
theorem finset.Ico.filter_le (n m l : ℕ) :
finset.filter (λ (x : ℕ), l ≤ x) (finset.Ico n m) = finset.Ico (max n l) m

source
@[simp]
theorem finset.Ico.diff_left (l n m : ℕ) :
finset.Ico n m \ finset.Ico n l = finset.Ico (max n l) m

source
@[simp]
theorem finset.Ico.diff_right (l n m : ℕ) :
finset.Ico n m \ finset.Ico l m = finset.Ico n (min m l)

source
theorem finset.Ico.image_const_sub {k m n : ℕ} (hkn : k ≤ n) :
finset.image (λ (j : ℕ), n - j) (finset.Ico k m) = finset.Ico (n + 1 - m) (n + 1 - k)

source
theorem finset.range_eq_Ico (n : ℕ) :
finset.range n = finset.Ico 0 n

source
theorem finset.range_image_pred_top_sub (n : ℕ) :
finset.image (λ (j : ℕ), n - 1 - j) (finset.range n) = finset.range n

source
def finset.Ico_ℤ (l u : ℤ) :
finset ℤ

Ico_ℤ l u is the set of integers l ≤ k < u.

Equations
source
@[simp]
theorem finset.Ico_ℤ.mem {n m l : ℤ} :
l ∈ finset.Ico_ℤ n m ↔ n ≤ l ∧ l < m

source
@[simp]
theorem finset.Ico_ℤ.card (l u : ℤ) :
(finset.Ico_ℤ l u).card = (u - l).to_nat