Documentation

Mathlib.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

Instances For

theorem Multiset.coe_range (n : ℕ) :

↑(List.range n) = range n

@[simp]

theorem Multiset.range_zero :

@[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