of_iso_comparison — Mathlib

English

If there is an isomorphism between G.obj ⊤ and ⊤, then G preserves terminal objects.

Русский

Если существует изоморфизм между G(⊤) и ⊤, то G сохраняет терминальные объекты.

LaTeX

$$$\\text{If } \\text{IsIso}(G(\\top_C) \\to \\top_D) \\text{ then } \\operatorname{PreservesLimit}(\\mathrm{empty}, G).$$$

Lean4

/-- If the terminal comparison map for `G` is an isomorphism, then `G` preserves terminal objects.
-/
theorem of_iso_comparison [i : IsIso (terminalComparison G)] : PreservesLimit (Functor.empty.{0} C) G :=
  by
  apply preservesLimit_of_preserves_limit_cone terminalIsTerminal
  apply (isLimitMapConeEmptyConeEquiv _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i

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