English
For s and f as above, removing duplicates from s before binding and then removing duplicates after binding yields the same result as binding first and then removing duplicates: dedup(bind(dedup(s), f)) = dedup(bind(s, f)).
Русский
Для s и f как выше удаление повторов из s до связывания и затем удаление повторов после связывания эквивалентно связыванию сначала и удалению повторов после: dedup(bind(dedup(s), f)) = dedup(bind(s, f)).
LaTeX
$$$(s.dedup).bind f.\dedup = (s.bind f).dedup$$$
Lean4
@[simp]
theorem dedup_bind_dedup [DecidableEq α] [DecidableEq β] (s : Multiset α) (f : α → Multiset β) :
(s.dedup.bind f).dedup = (s.bind f).dedup := by
ext x
simp_rw [count_dedup]
congr 1
simp
