mathlib documentation

data.multiset.intervals

Intervals in ℕ as multisets

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

Ico

def multiset.Ico  :

Ico n m is the multiset lifted from the list Ico n m, e.g. the set {n, n+1, ..., m-1}.

Equations
theorem multiset.Ico.map_add (n m k : ) :

theorem multiset.Ico.map_sub (n m k : ) :
k nmultiset.map (λ (x : ), x - k) (multiset.Ico n m) = multiset.Ico (n - k) (m - k)

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

theorem multiset.Ico.nodup (n m : ) :

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

theorem multiset.Ico.eq_zero_of_le {n m : } :
m nmultiset.Ico n m = 0

@[simp]
theorem multiset.Ico.self_eq_zero {n : } :

@[simp]
theorem multiset.Ico.eq_zero_iff {n m : } :
multiset.Ico n m = 0 m n

theorem multiset.Ico.add_consecutive {n m l : } :
n mm lmultiset.Ico n m + multiset.Ico m l = multiset.Ico n l

@[simp]

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

theorem multiset.Ico.succ_top {n m : } :
n mmultiset.Ico n (m + 1) = m ::ₘ multiset.Ico n m

theorem multiset.Ico.eq_cons {n m : } :
n < mmultiset.Ico n m = n ::ₘ multiset.Ico (n + 1) m

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

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

theorem multiset.Ico.filter_lt_of_top_le {n m l : } :
m lmultiset.filter (λ (x : ), x < l) (multiset.Ico n m) = multiset.Ico n m

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

theorem multiset.Ico.filter_le_of_bot {n m : } :
n < mmultiset.filter (λ (x : ), x n) (multiset.Ico n m) = {n}

theorem multiset.Ico.filter_lt_of_ge {n m l : } :
l mmultiset.filter (λ (x : ), x < l) (multiset.Ico n m) = multiset.Ico n l

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

theorem multiset.Ico.filter_le_of_le_bot {n m l : } :
l nmultiset.filter (λ (x : ), l x) (multiset.Ico n m) = multiset.Ico n m

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

theorem multiset.Ico.filter_le_of_le {n m l : } :
n lmultiset.filter (λ (x : ), l x) (multiset.Ico n m) = multiset.Ico l m

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