English
If two finite types α and β have the same cardinality, then there exists a genuine equivalence α ≃ β (noncomputable).
Русский
Если два конечных типа имеют одинаковую мощность, существует эквиваленция α ≃ β (невычислимая).
LaTeX
$$$\operatorname{card}\alpha = \operatorname{card}\beta \Rightarrow \alpha \simeq \beta.$$$
Lean4
/-- Two `Fintype`s with the same cardinality are (noncomputably) in bijection.
See `Fintype.truncEquivOfCardEq` for the computable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq` for
the specialization to `Fin`.
-/
noncomputable def equivOfCardEq (h : card α = card β) : α ≃ β :=
by
letI := Classical.decEq α
letI := Classical.decEq β
exact (truncEquivOfCardEq h).out
