mathlib documentation

data.multiset.range

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
@[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.range n).card = 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)