Multiset.card_range
theorem Multiset.card_range : ∀ (n : ℕ), Multiset.card (Multiset.range n) = n
This theorem states that for any natural number `n`, the cardinality of the multiset obtained by the `range` function from `n` (which represents the multiset containing numbers from 0 to `n-1`) is equal to `n`. In other words, the number of elements in the multiset `{0, 1, ..., n-1}` is `n`.
More concisely: The cardinality of the multiset generated by the `range` function from a natural number equals that natural number.
|
Multiset.range_subset
theorem Multiset.range_subset : ∀ {m n : ℕ}, Multiset.range m ⊆ Multiset.range n ↔ m ≤ n
The theorem `Multiset.range_subset` states that for any two natural numbers `m` and `n`, the multiset `range m`, which is the set of natural numbers from `0` to `m-1`, is a subset of the multiset `range n`, which is the set of natural numbers from `0` to `n-1`, if and only if `m` is less than or equal to `n`. Essentially, it's saying that the range of numbers up to `m` can only be contained in the range of numbers up to `n` if `m` is not greater than `n`.
More concisely: The theorem `Multiset.range_subset` asserts that for all natural numbers `m` and `n`, `range m` is a subset of `range n` if and only if `m <= n`.
|
Mathlib.Data.Multiset.Range._auxLemma.1
theorem Mathlib.Data.Multiset.Range._auxLemma.1 : ∀ {m n : ℕ}, (m ∈ Multiset.range n) = (m < n)
This theorem states that for all natural numbers `m` and `n`, `m` is an element of the multiset `Multiset.range n` if and only if `m` is less than `n`. This multiset is defined as the set of natural numbers from `0` to `n-1`. In other words, it establishes a relationship between the membership of a natural number in a particular multiset and its comparison with the size of that multiset.
More concisely: For all natural numbers `m` and `n`, `m` is an element of the multiset `Multiset.range n` if and only if `m < n`.
|