equivFinOfCardEq — Mathlib

English

If card α = n, there is a (noncomputable) bijection α ≃ Fin n.

Русский

Если card(α) = n, существует невычислимая биекция α ≃ Fin n.

LaTeX

$$$\operatorname{card}\alpha = n \Rightarrow \alpha \simeq \mathrm{Fin}(n).$$$

Lean4

/-- If the cardinality of `α` is `n`, there is noncomputably a bijection between `α` and `Fin n`.

See `Fintype.truncEquivFinOfCardEq` for the computable definition,
and `Fintype.truncEquivFin` and `Fintype.equivFin` for the bijection `α ≃ Fin (card α)`.
-/
noncomputable def equivFinOfCardEq {n : ℕ} (h : Fintype.card α = n) : α ≃ Fin n :=
  letI := Classical.decEq α
  (truncEquivFinOfCardEq h).out

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