Multiset.map_toEnumFinset_fst
theorem Multiset.map_toEnumFinset_fst :
∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Multiset.map Prod.fst m.toEnumFinset.val = m
This theorem states that for any multiset `m` of a type `α` with decidable equality, if you convert `m` to a finset whose elements enumerate the elements of the multiset (with `ℕ` component differentiating between equal elements), and then map the `fst` function (which extracts the first element of a pair) over this finset, you will get back the original multiset `m`. In other words, the process of transforming the multiset to an enumerated finset and then projecting out the first components of the finset is a lossless operation; it does not change the underlying multiset.
More concisely: For any decidably equated multiset `m` of type `α`, the mapping `fst ∘ toFinset (map finset.single m)` equals `m`.
|
Multiset.mem_toEnumFinset
theorem Multiset.mem_toEnumFinset :
∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (p : α × ℕ),
p ∈ m.toEnumFinset ↔ p.2 < Multiset.count p.1 m
This theorem, `Multiset.mem_toEnumFinset`, states that for any type `α` with a decidable equality and any multiset `m` of this type, a pair `p` (consisting of an element of `α` and a natural number) is a member of the finset obtained from `m` by the `toEnumFinset` function if and only if the second component of `p` is less than the count of the first component of `p` in `m`. In simpler terms, the theorem relates the membership of an element in a finset, derived from a multiset, to the count of that element in the original multiset.
More concisely: For any type `α` with decidable equality and any multiset `m` of `α`, an element `x` of `α` with a natural number `n` is a member of the finset obtained from `m` by `toEnumFinset` if and only if `n` is less than the count of `x` in `m`.
|
Multiset.map_univ_coe
theorem Multiset.map_univ_coe :
∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Multiset.map (fun x => x.fst) Finset.univ.val = m := by
sorry
The theorem `Multiset.map_univ_coe` states that for any type `α` with decidable equality and any multiset `m` of that type, mapping the function `(fun x => x.fst)` over the universal finite set (`Finset.univ.val`) results in the original multiset `m`. Here, `(fun x => x.fst)` is a function that takes a pair and returns the first element. Essentially, this theorem says that every element in the universal set can be paired with an element in the multiset `m`, and applying the map operation results in the same multiset `m`.
More concisely: For any type `α` with decidable equality and any multiset `m` of type `α`, the map operation `Multiset.map m (λ x, x.fst)` equals `m` itself.
|
Mathlib.Data.Multiset.Fintype._auxLemma.13
theorem Mathlib.Data.Multiset.Fintype._auxLemma.13 :
∀ {α : Type u_1} [inst : DecidableEq α] {m₁ m₂ : Multiset α}, (m₁.toEnumFinset ⊆ m₂.toEnumFinset) = (m₁ ≤ m₂) := by
sorry
The theorem `Mathlib.Data.Multiset.Fintype._auxLemma.13` states that for any two multisets `m₁` and `m₂` of a type `α` (where `α` is a type with decidable equality), the property that the `Finset` obtained by enumerating the elements of `m₁` (using `Multiset.toEnumFinset`) is a subset of the `Finset` obtained from `m₂` is equivalent to the property that `m₁` is a submultiset of `m₂`. In other words, `m₁` is a submultiset of `m₂` if and only if every element of `m₁`, each associated with its count in the multiset, appears in `m₂` with a count equal to or higher.
More concisely: For multisets `m₁` and `m₂` over a type `α` with decidable equality, `m₁` is a submultiset of `m₂` if and only if the finite set obtained from `m₁` equals the subset of the finite set obtained from `m₂` that includes each element of `m₁` with its corresponding multiplicity.
|