mathlib3 documentation

data.multiset.range

multiset.range n gives {0, 1, ..., n-1} as a multiset. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
def multiset.range (n : ℕ) :
multiset ℕ

range n is the multiset lifted from the list range n, that is, the set {0, 1, ..., n-1}.

Equations
source
theorem multiset.coe_range (n : ℕ) :
↑(list.range n) = multiset.range n
source
@[simp]
theorem multiset.range_zero  :
multiset.range 0 = 0
source
@[simp]
theorem multiset.range_succ (n : ℕ) :
multiset.range n.succ = n ::ₘ multiset.range n
source
@[simp]
theorem multiset.card_range (n : ℕ) :
⇑multiset.card (multiset.range n) = n
source
theorem multiset.range_subset {m n : ℕ} :
multiset.range m ⊆ multiset.range n ↔ m ≤ n
source
@[simp]
theorem multiset.mem_range {m n : ℕ} :
m ∈ multiset.range n ↔ m < n
source
@[simp]
theorem multiset.not_mem_range_self {n : ℕ} :
n ∉ multiset.range n
source
theorem multiset.self_mem_range_succ (n : ℕ) :
n ∈ multiset.range (n + 1)
source
theorem multiset.range_add (a b : ℕ) :
multiset.range (a + b) = multiset.range a + multiset.map (λ (x : ℕ), a + x) (multiset.range b)
source
theorem multiset.range_disjoint_map_add (a : ℕ) (m : multiset ℕ) :
(multiset.range a).disjoint (multiset.map (λ (x : ℕ), a + x) m)
source
theorem multiset.range_add_eq_union (a b : ℕ) :
multiset.range (a + b) = multiset.range a ∪ multiset.map (λ (x : ℕ), a + x) (multiset.range b)