English
The Finset version of bind (the monadic join) matches the algebraic biUnion after converting multisets to Finsets.
Русский
Эквивалентность bind и biUnion в Finset после приведения Multiset к Finset.
LaTeX
$$$(s.bind t).toFinset = s.toFinset.biUnion (\\lambda a, (t a).toFinset)$$$
Lean4
theorem bind_toFinset [DecidableEq α] (s : Multiset α) (t : α → Multiset β) :
(s.bind t).toFinset = s.toFinset.biUnion fun a ↦ (t a).toFinset :=
ext fun x ↦ by simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind]