mathlib documentation

data.multiset.range

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

def multiset.range (n : ℕ) :

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

Equations

multiset.range n = ↑(list.range n)

@[simp]

theorem multiset.range_zero :

multiset.range 0 = 0

@[simp]

theorem multiset.range_succ (n : ℕ) :

multiset.range n.succ = n ::ₘ multiset.range n

@[simp]

theorem multiset.card_range (n : ℕ) :

⇑multiset.card (multiset.range n) = n

theorem multiset.range_subset {m n : ℕ} :

multiset.range m ⊆ multiset.range n ↔ m ≤ n

@[simp]

theorem multiset.mem_range {m n : ℕ} :

m ∈ multiset.range n ↔ m < n

@[simp]

theorem multiset.not_mem_range_self {n : ℕ} :

n ∉ multiset.range n

theorem multiset.self_mem_range_succ (n : ℕ) :

n ∈ multiset.range (n + 1)

theorem multiset.range_add (a b : ℕ) :

multiset.range (a + b) = multiset.range a + multiset.map (λ (x : ℕ), a + x) (multiset.range b)

theorem multiset.range_disjoint_map_add (a : ℕ) (m : multiset ℕ) :

(multiset.range a).disjoint (multiset.map (λ (x : ℕ), a + x) m)

theorem multiset.range_add_eq_union (a b : ℕ) :

multiset.range (a + b) = multiset.range a ∪ multiset.map (λ (x : ℕ), a + x) (multiset.range b)