toFinset_dedup — Mathlib

English

Removing duplicates from a multiset before forming a Finset does not change the result of toFinset.

Русский

Удаление повторов из мультимножества перед образованием Finset не изменяет результат toFinset.

LaTeX

$$$\\forall {\\alpha} {m : \\mathsf{Multiset}\\,\\alpha}, m.dedup.toFinset = m.toFinset$$$

Lean4

@[simp]
theorem toFinset_dedup (m : Multiset α) : m.dedup.toFinset = m.toFinset := by simp_rw [toFinset, dedup_idem]

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