bind_toFinset — Mathlib

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]

Похожие утверждения