card_toEnumFinset — Mathlib

English

For any multiset m of α, the cardinality of its toEnumFinset equals the cardinality of m.

Русский

Для любого мультимножества m над α кардинальность m.toEnumFinset равна кардинальности m.

LaTeX

$$$\mathrm{card}(m.\mathrm{toEnumFinset}) = \mathrm{card}(m)$$$

Lean4

@[simp]
theorem card_toEnumFinset (m : Multiset α) : m.toEnumFinset.card = Multiset.card m :=
  by
  rw [Finset.card, ← Multiset.card_map Prod.fst m.toEnumFinset.val]
  congr
  exact m.map_toEnumFinset_fst

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