English
For any finitely supported function f, the finset obtained from toMultiset(f) equals the support of f (with decidable equality). In symbols: toMultiset(f).toFinset = f.support.
Русский
Для произвольной функции с конечной опорой искомое множество элементов — это поддержка функции: toMultiset(f).toFinset = f.support.
LaTeX
$$$\mathrm{toFinset}\bigl(\mathrm{toMultiset}(f)\bigr) = \mathrm{support}(f)$$$
Lean4
@[simp]
theorem toFinset_toMultiset [DecidableEq α] (f : α →₀ ℕ) : f.toMultiset.toFinset = f.support :=
by
refine f.induction ?_ ?_
· rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
· intro a n f ha hn ih
rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq, support_single_ne_zero _ hn,
Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
refine Disjoint.mono_left support_single_subset ?_
rwa [Finset.disjoint_singleton_left]
