card_eq_fintypeCard — Mathlib

English

The cardinality of α equals the standard Fintype cardinality when α is FinEnum.

Русский

Кардинальность α равна стандартной кардинальности Fintype, если α — FinEnum.

LaTeX

$$$ \\operatorname{card}(\\\\alpha) = \\operatorname{Fintype.card}(\\\\alpha). $$$

Lean4

/-- The enumeration merely adds an ordering, leaving the cardinality as is. -/
theorem card_eq_fintypeCard {α : Type u} [FinEnum α] [Fintype α] : card α = Fintype.card α :=
  Fintype.truncEquivFin α |>.inductionOn (fun h ↦ Fin.equiv_iff_eq.mp ⟨equiv.symm.trans h⟩)

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