card_coe — Mathlib

English

The cardinality of the finite type associated to a multiset m coincides with the multiset cardinality of m; i.e., the number of elements in m.ToType equals the number of elements in m.

Русский

Кардинал связанного с мультимножество типа совпадает с кардиналом самого мультимножества; то есть число элементов в m.ToType равно числу элементов в m.

LaTeX

$$$\mathrm{Fintype.card}(m.\mathrm{ToType}) = \mathrm{Multiset.card}(m)$$$

Lean4

@[simp]
theorem card_coe (m : Multiset α) : Fintype.card m = Multiset.card m :=
  by
  rw [Fintype.card_congr m.coeEquiv]
  simp only [Fintype.card_coe, card_toEnumFinset]

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