instFintype — Mathlib

English

Equivalences α ≃ β between finite types form a finite type.

Русский

Эквиваленты α ≃ β между конечными типами образуют конечный тип.

LaTeX

$$$Fintype (\\alpha \\simeq \\beta)$$$

Lean4

instance instFintype [Fintype α] [Fintype β] : Fintype (α ≃ β) :=
  if h : Fintype.card β = Fintype.card α then
    Trunc.recOnSubsingleton (Fintype.truncEquivFin α) fun eα =>
      Trunc.recOnSubsingleton (Fintype.truncEquivFin β) fun eβ =>
        @Fintype.ofEquiv _ (Perm α) fintypePerm
          (equivCongr (Equiv.refl α) (eα.trans (Eq.recOn h eβ.symm)) : α ≃ α ≃ (α ≃ β))
  else ⟨∅, fun x => False.elim (h (Fintype.card_eq.2 ⟨x.symm⟩))⟩

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