is_skeletal — Mathlib

English

FintypeCat.Skeleton is skeletal, i.e., every object is isomorphic to a canonical mk(len(X)).

Русский

FintypeCat.Skeleton является скелетом: каждый объект изоморфен каноническому mk(len(X)).

LaTeX

$$$\\forall X:\\text{Skeleton},\\; X \\cong \\text{mk}(\\mathrm{len}(X))$$$

Lean4

theorem is_skeletal : Skeletal Skeleton.{u} := fun X Y ⟨h⟩ =>
  ext _ _ <|
    Fin.equiv_iff_eq.mp <|
      Nonempty.intro <|
        { toFun := fun x => (h.hom ⟨x⟩).down
          invFun := fun x => (h.inv ⟨x⟩).down
          left_inv := by
            intro a
            change ULift.down _ = _
            rw [ULift.up_down]
            change ((h.hom ≫ h.inv) _).down = _
            simp
            rfl
          right_inv := by
            intro a
            change ULift.down _ = _
            rw [ULift.up_down]
            change ((h.inv ≫ h.hom) _).down = _
            simp
            rfl }

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