Mathlib.Data.Multiset.Range

Multiset.range definition

(n : ℕ) : Multiset ℕ

Full source

/-- `range n` is the multiset lifted from the list `range n`,
  that is, the set `{0, 1, ..., n-1}`. -/
def range (n : ℕ) : Multiset ℕ :=
  List.range n

Multiset of numbers from 0 to $ n-1 $

Informal description

For a natural number $ n $, the multiset `range n` is the multiset version of the list containing the numbers $ \{0, 1, \ldots, n-1\} $.

Multiset.coe_range theorem

(n : ℕ) : ↑(List.range n) = range n

Full source

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

Lifting of List Range to Multiset Equals Multiset Range

Informal description

For any natural number $n$, the canonical lifting of the list `[0, 1, ..., n-1]` to a multiset is equal to the multiset `range n`.

Multiset.range_zero theorem

: range 0 = 0

Full source

@[simp]
theorem range_zero : range 0 = 0 :=
  rfl

Empty multiset range: $\text{range}(0) = 0$

Informal description

The multiset $\{0, 1, \ldots, n-1\}$ for $n = 0$ is equal to the empty multiset $0$.

Multiset.range_succ theorem

(n : ℕ) : range (succ n) = n ::ₘ range n

Full source

@[simp]
theorem range_succ (n : ℕ) : range (succ n) = n ::ₘ range n := by
  rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]

Recursive construction of multiset range: $\text{range}(n+1) = n \mathbin{::} \text{range}(n)$

Informal description

For any natural number $n$, the multiset $\{0, 1, \ldots, n\}$ is equal to the multiset obtained by inserting $n$ into the multiset $\{0, 1, \ldots, n-1\}$.

Multiset.card_range theorem

(n : ℕ) : card (range n) = n

Full source

@[simp]
theorem card_range (n : ℕ) : card (range n) = n :=
  length_range

Cardinality of the multiset $\{0, 1, \ldots, n-1\}$ is $n$

Informal description

For any natural number $n$, the cardinality of the multiset $\{0, 1, \ldots, n-1\}$ is equal to $n$.

Multiset.range_subset theorem

{m n : ℕ} : range m ⊆ range n ↔ m ≤ n

Full source

theorem range_subset {m n : ℕ} : rangerange m ⊆ range nrange m ⊆ range n ↔ m ≤ n :=
  List.range_subset

Subset Relation Between Multiset Ranges and Natural Number Ordering

Informal description

For any natural numbers $m$ and $n$, the multiset $\{0, 1, \ldots, m-1\}$ is a subset of the multiset $\{0, 1, \ldots, n-1\}$ if and only if $m \leq n$.

Multiset.mem_range theorem

{m n : ℕ} : m ∈ range n ↔ m < n

Full source

@[simp]
theorem mem_range {m n : ℕ} : m ∈ range nm ∈ range n ↔ m < n :=
  List.mem_range

Membership in Multiset Range: $m \in \{0, \ldots, n-1\} \leftrightarrow m < n$

Informal description

For natural numbers $m$ and $n$, the element $m$ belongs to the multiset $\{0, 1, \ldots, n-1\}$ if and only if $m < n$.

Multiset.not_mem_range_self theorem

{n : ℕ} : n ∉ range n

Full source

theorem not_mem_range_self {n : ℕ} : n ∉ range n :=
  List.not_mem_range_self

$n \notin \{0, \ldots, n-1\}$ for natural numbers

Informal description

For any natural number $n$, the element $n$ does not belong to the multiset $\{0, 1, \ldots, n-1\}$.

Multiset.self_mem_range_succ theorem

(n : ℕ) : n ∈ range (n + 1)

Full source

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

$n \in \{0, 1, \ldots, n\}$ for natural numbers

Informal description

For any natural number $n$, the element $n$ is contained in the multiset $\{0, 1, \ldots, n\}$.

Multiset.range_add theorem

(a b : ℕ) : range (a + b) = range a + (range b).map (a + ·)

Full source

theorem range_add (a b : ℕ) : range (a + b) = range a + (range b).map (a + ·) :=
  congr_arg ((↑) : List ℕ → Multiset ℕ) List.range_add

Additivity of Multiset Range: $\text{range}(a + b) = \text{range}(a) + \text{range}(b).\text{map} (a + \cdot)$

Informal description

For any natural numbers $a$ and $b$, the multiset $\{0, 1, \ldots, a + b - 1\}$ is equal to the sum of the multiset $\{0, 1, \ldots, a - 1\}$ and the multiset obtained by adding $a$ to each element of $\{0, 1, \ldots, b - 1\}$. In symbols: \[ \text{range}(a + b) = \text{range}(a) + \text{range}(b).\text{map} (a + \cdot) \]

Multiset.range_disjoint_map_add theorem

(a : ℕ) (m : Multiset ℕ) : Disjoint (range a) (m.map (a + ·))

Full source

theorem range_disjoint_map_add (a : ℕ) (m : Multiset ℕ) :
    Disjoint (range a) (m.map (a + ·)) := by
  rw [disjoint_left]
  intro x hxa hxb
  rw [range, mem_coe, List.mem_range] at hxa
  obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
  exact (Nat.le_add_right _ _).not_lt hxa

Disjointness of Range and Shifted Multiset: $\text{range}(a) \cap (a + m) = \emptyset$

Informal description

For any natural number $a$ and any multiset $m$ of natural numbers, the multiset $\{0, 1, \ldots, a-1\}$ is disjoint from the multiset obtained by adding $a$ to each element of $m$. In other words, no element of $\{0, 1, \ldots, a-1\}$ is of the form $a + x$ for some $x \in m$.

Multiset.range_add_eq_union theorem

(a b : ℕ) : range (a + b) = range a ∪ (range b).map (a + ·)

Full source

theorem range_add_eq_union (a b : ℕ) : range (a + b) = rangerange a ∪ (range b).map (a + ·) := by
  rw [range_add, add_eq_union_iff_disjoint]
  apply range_disjoint_map_add

Union Decomposition of Multiset Range: $\text{range}(a + b) = \text{range}(a) \cup (a + \text{range}(b))$

Informal description

For any natural numbers $a$ and $b$, the multiset $\{0, 1, \ldots, a + b - 1\}$ is equal to the union of the multiset $\{0, 1, \ldots, a - 1\}$ and the multiset obtained by adding $a$ to each element of $\{0, 1, \ldots, b - 1\}$. In symbols: \[ \text{range}(a + b) = \text{range}(a) \cup \{a + x \mid x \in \text{range}(b)\} \]

Multiset.nodup_range theorem

(n : ℕ) : Nodup (range n)

Full source

theorem nodup_range (n : ℕ) : Nodup (range n) :=
  List.nodup_range

No Duplicates in Multiset $\{0, 1, \ldots, n-1\}$

Informal description

For any natural number $n$, the multiset $\{0, 1, \ldots, n-1\}$ has no duplicate elements.

Multiset.range_le theorem

{m n : ℕ} : range m ≤ range n ↔ m ≤ n

Full source

theorem range_le {m n : ℕ} : rangerange m ≤ range n ↔ m ≤ n :=
  (le_iff_subset (nodup_range _)).trans range_subset

Multiset Range Ordering: $\{0, \ldots, m-1\} \leq \{0, \ldots, n-1\} \leftrightarrow m \leq n$

Informal description

For any natural numbers $m$ and $n$, the multiset $\{0, 1, \ldots, m-1\}$ is less than or equal to the multiset $\{0, 1, \ldots, n-1\}$ in the multiset order if and only if $m \leq n$.