truncEquivFin — Mathlib

English

There is a computable equivalence between α and Fin(card α), but it is wrapped in a truncation to preserve computability.

Русский

Существует вычислимая эквиваленция между α и Fin(card α), но она обернута в трюк (trunc) для сохранения вычислимости.

LaTeX

$$$\mathrm{Trunc}\bigl(\alpha \simeq \mathrm{Fin}(\mathrm{card}\,\alpha)\bigr).$$$

Lean4

/-- There is (computably) an equivalence between `α` and `Fin (card α)`.

Since it is not unique and depends on which permutation
of the universe list is used, the equivalence is wrapped in `Trunc` to
preserve computability.

See `Fintype.equivFin` for the noncomputable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq`
for an equiv `α ≃ Fin n` given `Fintype.card α = n`.

See `Fintype.truncFinBijection` for a version without `[DecidableEq α]`.
-/
def truncEquivFin (α) [DecidableEq α] [Fintype α] : Trunc (α ≃ Fin (card α)) :=
  by
  unfold card Finset.card
  exact
    Quot.recOnSubsingleton (motive := fun s : Multiset α =>
      (∀ x : α, x ∈ s) → s.Nodup → Trunc (α ≃ Fin (Multiset.card s))) univ.val
      (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getEquivOfForallMemList _ h).symm) mem_univ_val univ.2

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