Intervals in ℕ as multisets
For now this only covers Ico n m, the "closed-open" interval containing [n, ..., m-1].
Ico
Ico n m is the multiset lifted from the list Ico n m, e.g. the set {n, n+1, ..., m-1}.
Equations
- multiset.Ico n m = ↑(list.Ico n m)
theorem
multiset.Ico.map_add
(n m k : ℕ) :
multiset.map (has_add.add k) (multiset.Ico n m) = multiset.Ico (n + k) (m + k)
theorem
multiset.Ico.map_sub
(n m k : ℕ) :
k ≤ n → multiset.map (λ (x : ℕ), x - k) (multiset.Ico n m) = multiset.Ico (n - k) (m - k)
theorem
multiset.Ico.add_consecutive
{n m l : ℕ} :
n ≤ m → m ≤ l → multiset.Ico n m + multiset.Ico m l = multiset.Ico n l
@[simp]
@[simp]
theorem
multiset.Ico.filter_lt_of_top_le
{n m l : ℕ} :
m ≤ l → multiset.filter (λ (x : ℕ), x < l) (multiset.Ico n m) = multiset.Ico n m
theorem
multiset.Ico.filter_lt_of_le_bot
{n m l : ℕ} :
l ≤ n → multiset.filter (λ (x : ℕ), x < l) (multiset.Ico n m) = ∅
theorem
multiset.Ico.filter_le_of_bot
{n m : ℕ} :
n < m → multiset.filter (λ (x : ℕ), x ≤ n) (multiset.Ico n m) = {n}
theorem
multiset.Ico.filter_lt_of_ge
{n m l : ℕ} :
l ≤ m → multiset.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 ≤ n → multiset.filter (λ (x : ℕ), l ≤ x) (multiset.Ico n m) = multiset.Ico n m
theorem
multiset.Ico.filter_le_of_top_le
{n m l : ℕ} :
m ≤ l → multiset.filter (λ (x : ℕ), l ≤ x) (multiset.Ico n m) = ∅
theorem
multiset.Ico.filter_le_of_le
{n m l : ℕ} :
n ≤ l → multiset.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