equivFinOfCardEq — Mathlib

English

Let α be a finite-type and n ∈ ℕ. If card(α) = n, then α is in bijection with Fin n.

Русский

Пусть α конечного типа и n ∈ ℕ. Если card(α) = n, то существует биекция α ≃ Fin n.

LaTeX

$$$\mathrm{card}(\alpha) = n \Rightarrow \alpha \cong Fin\,n$$$

Lean4

/-- Similar to `Finite.equivFin` but with control over the term used for the cardinality. -/
def equivFinOfCardEq [Finite α] {n : ℕ} (h : Nat.card α = n) : α ≃ Fin n :=
  by
  subst h
  apply Finite.equivFin

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