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

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)

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

@[simp]

theorem Multiset.range_zero : range 0 = 0

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem Multiset.notMem_range_self {n : ℕ} : n ∉ range n

@[deprecated Multiset.notMem_range_self (since := "2025-05-23")]

theorem Multiset.not_mem_range_self {n : ℕ} : n ∉ range n

Alias of Multiset.notMem_range_self.

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

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

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

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

theorem Multiset.nodup_range (n : ℕ) : (range n).Nodup

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