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 #

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

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

Equations
source
theorem multiset.Ico.map_add (n m k : ℕ) :
multiset.map (has_add.add k) (multiset.Ico n m) = multiset.Ico (n + k) (m + k)
source
theorem multiset.Ico.map_sub (n m k : ℕ) (h : k ≤ n) :
multiset.map (λ (x : ℕ), x - k) (multiset.Ico n m) = multiset.Ico (n - k) (m - k)
source
theorem multiset.Ico.zero_bot (n : ℕ) :
multiset.Ico 0 n = multiset.range n
source
@[simp]
theorem multiset.Ico.card (n m : ℕ) :
⇑multiset.card (multiset.Ico n m) = m - n
source
theorem multiset.Ico.nodup (n m : ℕ) :
(multiset.Ico n m).nodup
source
@[simp]
theorem multiset.Ico.mem {n m l : ℕ} :
l ∈ multiset.Ico n m ↔ n ≤ l ∧ l < m
source
theorem multiset.Ico.eq_zero_of_le {n m : ℕ} (h : m ≤ n) :
multiset.Ico n m = 0
source
@[simp]
theorem multiset.Ico.self_eq_zero {n : ℕ} :
multiset.Ico n n = 0
source
@[simp]
theorem multiset.Ico.eq_zero_iff {n m : ℕ} :
multiset.Ico n m = 0 ↔ m ≤ n
source
theorem multiset.Ico.add_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) :
multiset.Ico n m + multiset.Ico m l = multiset.Ico n l
source
@[simp]
theorem multiset.Ico.inter_consecutive (n m l : ℕ) :
multiset.Ico n m ∩ multiset.Ico m l = 0
source
@[simp]
theorem multiset.Ico.succ_singleton {n : ℕ} :
multiset.Ico n (n + 1) = {n}
source
theorem multiset.Ico.succ_top {n m : ℕ} (h : n ≤ m) :
multiset.Ico n (m + 1) = m ::ₘ multiset.Ico n m
source
theorem multiset.Ico.eq_cons {n m : ℕ} (h : n < m) :
multiset.Ico n m = n ::ₘ multiset.Ico (n + 1) m
source
@[simp]
theorem multiset.Ico.pred_singleton {m : ℕ} (h : 0 < m) :
multiset.Ico (m - 1) m = {m - 1}
source
@[simp]
theorem multiset.Ico.not_mem_top {n m : ℕ} :
m ∉ multiset.Ico n m
source
theorem multiset.Ico.filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) :
multiset.filter (λ (x : ℕ), x < l) (multiset.Ico n m) = multiset.Ico n m
source
theorem multiset.Ico.filter_lt_of_le_bot {n m l : ℕ} (hln : l ≤ n) :
multiset.filter (λ (x : ℕ), x < l) (multiset.Ico n m) = ∅
source
theorem multiset.Ico.filter_le_of_bot {n m : ℕ} (hnm : n < m) :
multiset.filter (λ (x : ℕ), x ≤ n) (multiset.Ico n m) = {n}
source
theorem multiset.Ico.filter_lt_of_ge {n m l : ℕ} (hlm : l ≤ m) :
multiset.filter (λ (x : ℕ), x < l) (multiset.Ico n m) = multiset.Ico n l
source
@[simp]
theorem multiset.Ico.filter_lt (n m l : ℕ) :
multiset.filter (λ (x : ℕ), x < l) (multiset.Ico n m) = multiset.Ico n (min m l)
source
theorem multiset.Ico.filter_le_of_le_bot {n m l : ℕ} (hln : l ≤ n) :
multiset.filter (λ (x : ℕ), l ≤ x) (multiset.Ico n m) = multiset.Ico n m
source
theorem multiset.Ico.filter_le_of_top_le {n m l : ℕ} (hml : m ≤ l) :
multiset.filter (λ (x : ℕ), l ≤ x) (multiset.Ico n m) = ∅
source
theorem multiset.Ico.filter_le_of_le {n m l : ℕ} (hnl : n ≤ l) :
multiset.filter (λ (x : ℕ), l ≤ x) (multiset.Ico n m) = multiset.Ico l m
source
@[simp]
theorem multiset.Ico.filter_le (n m l : ℕ) :
multiset.filter (λ (x : ℕ), l ≤ x) (multiset.Ico n m) = multiset.Ico (max n l) m