Finsupp.count_toMultiset
theorem Finsupp.count_toMultiset :
∀ {α : Type u_1} [inst : DecidableEq α] (f : α →₀ ℕ) (a : α), Multiset.count a (Finsupp.toMultiset f) = f a := by
sorry
The theorem `Finsupp.count_toMultiset` states that for any type `α` with decidable equality, and for any function `f` from `α` to non-negative integers, and for any element `a` of `α`, the count of `a` in the multiset derived from `f` using `Finsupp.toMultiset` is equal to the value of `f` at `a`. In other words, the multiplicity of an element in the multiset that is converted from a function using `Finsupp.toMultiset` is the same as the value of the function at that element.
More concisely: For any function `f` from type `α` to non-negative integers with decidable equality, the count of `a` in the multiset `Finsupp.toMultiset f` is equal to `f a`.
|
Finsupp.toMultiset_single
theorem Finsupp.toMultiset_single : ∀ {α : Type u_1} (a : α) (n : ℕ), (Finsupp.toMultiset fun₀ | a => n) = n • {a} := by
sorry
The theorem `Finsupp.toMultiset_single` states that for any type `α`, any element `a` of that type, and any natural number `n`, the transformation `Finsupp.toMultiset` applied to the function that maps `a` to `n` (and anything else to zero) is equivalent to `n` copies of the multiset containing just `a`. In other words, creating a function that maps only one element to `n` and then converting this to a Multiset via `Finsupp.toMultiset` is the same as creating a multiset with `n` occurrences of that element.
More concisely: For any type `α`, the function mapping an element `a` of `α` to natural number `n`, and everything else to zero, and its corresponding multiset obtained via `Finsupp.toMultiset`, both contain `n` occurrences of `a`.
|
Finsupp.lt_wf
theorem Finsupp.lt_wf : ∀ (ι : Type u_3), WellFounded LT.lt
This theorem states that for any type `ι`, the less-than relation (`LT.lt`) on the function space from `ι` to the natural numbers (`ι →₀ ℕ`) is well-founded. In the context of set theory, a relation is well-founded if there are no infinite descending sequences, which means you can't continue infinitely picking `n+1`th elements that are 'smaller' than the `n`th elements. In other words, this theorem assures that if we have a sequence of functions from `ι` to the natural numbers, we can't keep finding a function that is 'smaller' than the previous one indefinitely.
More concisely: The relation `LT` on the function space `ι →₀ ℕ` from a type `ι` to the natural numbers is a well-founded relation.
|
Finsupp.toMultiset_add
theorem Finsupp.toMultiset_add :
∀ {α : Type u_1} (m n : α →₀ ℕ), Finsupp.toMultiset (m + n) = Finsupp.toMultiset m + Finsupp.toMultiset n := by
sorry
The theorem `Finsupp.toMultiset_add` states that for all types `α` and for any two functions `m` and `n` mapping from `α` to the natural numbers, converting the sum of `m` and `n` (under the function addition operation) to a multiset using `Finsupp.toMultiset` is equivalent to converting `m` and `n` separately to multisets and then adding the resulting multisets. In other words, the `Finsupp.toMultiset` function preserves the addition operation.
More concisely: For all types α and functions m, n from α to ℕ, Finsupp.toMultiset (m + n) = Finsupp.toMultiset m ⊕ Finsupp.toMultiset n.
|
Finsupp.toMultiset_zero
theorem Finsupp.toMultiset_zero : ∀ {α : Type u_1}, Finsupp.toMultiset 0 = 0
The theorem `Finsupp.toMultiset_zero` states that for any type `α`, the `Finsupp.toMultiset` function applied to the zero finitely supported function (or `finsupp`) results in the zero multiset. In other words, when there are no elements in the domain `α` with non-zero natural number values (as given by the zero `finsupp`), the resulting multiset (a generalization of sets that includes multiple instances of elements) is also empty.
More concisely: For any type `α`, the `Finsupp.toMultiset` of the zero finitely supported function is the empty multiset.
|