truncEquivFinOfCardEq — Mathlib

English

If α has card α = n, there is a truncated equivalence α ≃ Fin n computably.

Русский

Если карта α равна n, то существует трюк-эквиваленция α ≃ Fin n вычислительно.

LaTeX

$$$[\DecidableEq\ α] \ {n:\mathbb{N}}\ (\mathrm{card}\, \alpha = n) \Rightarrow \mathrm{Trunc}(\alpha \simeq \mathrm{Fin}(n)).$$$

Lean4

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

See `Fintype.equivFinOfCardEq` for the noncomputable definition,
and `Fintype.truncEquivFin` and `Fintype.equivFin` for the bijection `α ≃ Fin (card α)`.
-/
def truncEquivFinOfCardEq [DecidableEq α] {n : ℕ} (h : Fintype.card α = n) : Trunc (α ≃ Fin n) :=
  (truncEquivFin α).map fun e => e.trans (finCongr h)

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