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

def finset.Ico (n m : ) :

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

Equations
@[simp]
theorem finset.Ico.val (n m : ) :

@[simp]

theorem finset.Ico.image_add (n m k : ) :

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)

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

@[simp]
theorem finset.Ico.mem {n m l : } :
l finset.Ico n m n l l < m

@[simp]
theorem finset.Ico.coe_eq_Ico {n m : } :

theorem finset.Ico.eq_empty_of_le {n m : } (h : m n) :

@[simp]

@[simp]
theorem finset.Ico.eq_empty_iff {n m : } :

theorem finset.Ico.subset_iff {m₁ n₁ m₂ n₂ : } (hmn : m₁ < n₁) :
finset.Ico m₁ n₁ finset.Ico m₂ n₂ m₂ m₁ n₁ n₂

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

theorem finset.Ico.union_consecutive {n m l : } (hnm : n m) (hml : m l) :

theorem finset.Ico.union' {n m l k : } (hlm : l m) (hnk : n k) :

theorem finset.Ico.union {n m l k : } (h₁ : min n m max l k) (h₂ : min l k max n m) :

@[simp]

theorem finset.Ico.inter {n m l k : } :

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

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

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

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

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

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

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

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

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

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

@[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 : } (hln : 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 : } (hml : m l) :
finset.filter (λ (x : ), l x) (finset.Ico n m) =

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

@[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 : ) :

@[simp]
theorem finset.Ico.diff_right (l n m : ) :

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)

def finset.Ico_ℤ (l u : ) :

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

Equations
@[simp]
theorem finset.Ico_ℤ.mem {n m l : } :
l finset.Ico_ℤ n m n l l < m

@[simp]
theorem finset.Ico_ℤ.card (l u : ) :