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

ink

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

• Multiset.range n = ↑(List.range n)

ink

theorem Multiset.coe_range (n : ℕ) : ↑(List.range n) = Multiset.range n

ink

@[simp]

theorem Multiset.range_zero : Multiset.range 0 = 0

ink

@[simp]

theorem Multiset.range_succ (n : ℕ) : Multiset.range (Nat.succ n) = n ::ₘ Multiset.range n

ink

@[simp]

theorem Multiset.card_range (n : ℕ) : ↑Multiset.card (Multiset.range n) = n

ink

theorem Multiset.range_subset {m : ℕ} {n : ℕ} : Multiset.range m ⊆ Multiset.range n ↔ m ≤ n

ink

@[simp]

theorem Multiset.mem_range {m : ℕ} {n : ℕ} : m ∈ Multiset.range n ↔ m < n

ink

theorem Multiset.not_mem_range_self {n : ℕ} : ¬n ∈ Multiset.range n

ink

theorem Multiset.self_mem_range_succ (n : ℕ) : n ∈ Multiset.range (n + 1)

ink

theorem Multiset.range_add (a : ℕ) (b : ℕ) : Multiset.range (a + b) = Multiset.range a + Multiset.map (fun x => a + x) (Multiset.range b)

ink

theorem Multiset.range_disjoint_map_add (a : ℕ) (m : Multiset ℕ) : Multiset.Disjoint (Multiset.range a) (Multiset.map (fun x => a + x) m)

ink

theorem Multiset.range_add_eq_union (a : ℕ) (b : ℕ) : Multiset.range (a + b) = Multiset.range a ∪ Multiset.map (fun x => a + x) (Multiset.range b)