isIso_of_isTerminal — Mathlib

English

Any morphism between terminal objects is an isomorphism.

Русский

Любой морфизм между терминальными объектами является изоморфизмом.

LaTeX

$$$\\forall X,Y,\\text{IsTerminal } X, \\text{IsTerminal } Y \\Rightarrow \\text{IsIso }(f:X\\to Y)$$$

Lean4

/-- Any morphism between terminal objects is an isomorphism. -/
theorem isIso_of_isTerminal {X Y : C} (hX : IsTerminal X) (hY : IsTerminal Y) (f : X ⟶ Y) : IsIso f :=
  by
  refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩
  simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]
  apply IsTerminal.hom_ext hY

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