English
For a decidable-equipped α, and f : α →₀ ℕ, the number of occurrences of a is f a in the multiset toMultiset f: (toMultiset f).count a = f a.
Русский
Пусть α обладает DecidableEq, тогда для f : α →₀ ℕ число вхождений a в toMultiset f равно f a: (toMultiset f).count a = f a.
LaTeX
$$$(\mathrm{toMultiset} f).\mathrm{count}\; a = f(a)$$$
Lean4
@[simp]
theorem count_toMultiset [DecidableEq α] (f : α →₀ ℕ) (a : α) : (toMultiset f).count a = f a :=
calc
(toMultiset f).count a = Finsupp.sum f (fun x n => (n • { x } : Multiset α).count a) := by rw [toMultiset_apply];
exact map_sum (Multiset.countAddMonoidHom a) _ f.support
_ = f.sum fun x n => n * ({ x } : Multiset α).count a := by simp only [Multiset.count_nsmul]
_ = f a * ({ a } : Multiset α).count a :=
(sum_eq_single _ (fun a' _ H => by simp only [Multiset.count_singleton, if_false, H.symm, mul_zero])
(fun _ => zero_mul _))
_ = f a := by rw [Multiset.count_singleton_self, mul_one]
