card_unique — Mathlib

English

Any two enumerations of the same type α have the same length.

Русский

Любые два перечисления одного типа α имеют одну и ту же длину.

LaTeX

$$$ \\forall e_1 e_2:\\mathrm{FinEnum}\\alpha,\\ e_1.\\mathrm{card}\\alpha = e_2.\\mathrm{card}\\alpha. $$$

Lean4

/-- Any two enumerations of the same type have the same length. -/
theorem card_unique {α : Type u} (e₁ e₂ : FinEnum α) : e₁.card = e₂.card :=
  calc
    _
    _ = _ := (@card_eq_fintypeCard _ e₁ inferInstance)
    _ = _ := (Fintype.card_congr' rfl)
    _ = _ := @card_eq_fintypeCard _ e₂ inferInstance |>.symm

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