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  :
finset

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 : ) :
k nfinset.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

theorem finset.Ico.eq_empty_of_le {n m : } :
m nfinset.Ico n m =

@[simp]

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

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 mm lfinset.Ico n m finset.Ico m l = finset.Ico n l

@[simp]

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

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

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

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

@[simp]
theorem finset.Ico.pred_singleton {m : } :
0 < mfinset.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 : } :
m lfinset.filter (λ (x : ), x < l) (finset.Ico n m) = finset.Ico n m

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

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

theorem finset.Ico.filter_lt_of_ge {n m l : } :
l mfinset.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 nfinset.filter (λ (x : ), l x) (finset.Ico n m) = finset.Ico n m

theorem finset.Ico.filter_le_of_top_le {n m l : } :
m lfinset.filter (λ (x : ), l x) (finset.Ico n m) =

theorem finset.Ico.filter_le_of_le {n m l : } :
n lfinset.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 : } :
k nfinset.image (λ (j : ), n - j) (finset.Ico k m) = finset.Ico (n + 1 - m) (n + 1 - k)

def finset.Ico_ℤ  :
finset

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