equivFin — Mathlib

English

There is a canonical equivalence between a finite type α and Fin (Nat.card α).

Русский

Существует каноническая эквивалентность между конечным типом α и Fin (Nat.card α).

LaTeX

$$$ \\alpha\\ \\text{ is finite} \\Rightarrow \\alpha \\cong Fin (Nat.card\\, \\alpha). $$$

Lean4

/-- There is (noncomputably) an equivalence between a finite type `α` and `Fin (Nat.card α)`. -/
def equivFin (α : Type*) [Finite α] : α ≃ Fin (Nat.card α) :=
  by
  have := (Finite.exists_equiv_fin α).choose_spec.some
  rwa [Nat.card_eq_of_equiv_fin this]

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