Multiset.toDFinsupp_injective
theorem Multiset.toDFinsupp_injective :
∀ {α : Type u_1} [inst : DecidableEq α], Function.Injective ⇑Multiset.toDFinsupp
The theorem `Multiset.toDFinsupp_injective` states that for any type `α` which has decidable equality, the function `Multiset.toDFinsupp` is injective. In other words, if `Multiset.toDFinsupp` applied to two multiset `α` objects produces the same result, then those two multisets were identical. This function `Multiset.toDFinsupp` converts a multiset into a DFinsupp, which is a type of function from elements of `α` to natural numbers, basically representing the count of each element in the multiset.
More concisely: For any decidably equal multisets of type `α`, their conversion to DFinsupps using `Multiset.toDFinsupp` results in equal functions.
|
DFinsupp.toMultiset_toDFinsupp
theorem DFinsupp.toMultiset_toDFinsupp :
∀ {α : Type u_1} [inst : DecidableEq α] (f : Π₀ (x : α), ℕ), Multiset.toDFinsupp (DFinsupp.toMultiset f) = f := by
sorry
This theorem states that for any type `α` that has decidable equality, given a function `f` mapping each element in `α` to a natural number (as a direct sum), the operation of first converting `f` to a multiset using `DFinsupp.toMultiset` and then back to a function using `Multiset.toDFinsupp` is the identity operation on `f`. In other words, going from a direct sum to a multiset and back leaves the original direct sum function `f` unchanged.
More concisely: For any type `α` with decidable equality, the function `DFinsupp.toMultiset ∘ DFinsupp.fromMultiset` is the identity on functions from `α` to the natural numbers as direct sums.
|