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.Ico n m).card = 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