fintypeEquivFin — Mathlib

English

Every encodable finite type α is bijectively equivalent to the finite set Fin(card α).

Русский

Каждый кодируемый конечный тип α эквивалентен по биекции конечному множеству Fin(card α).

LaTeX

$$$\alpha \simeq Fin(|\alpha|)$$$

Lean4

/-- An encodable `Fintype` is equivalent to the same size `Fin`. -/
def fintypeEquivFin {α} [Fintype α] [Encodable α] : α ≃ Fin (Fintype.card α) :=
  haveI : DecidableEq α := Encodable.decidableEqOfEncodable _
  ((sortedUniv_nodup α).getEquivOfForallMemList _ mem_sortedUniv).symm.trans <|
    Equiv.cast (congr_arg _ (length_sortedUniv α))

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