preservesLimit_empty_of_isIso_terminalComparison

English

If terminalComparison F is an isomorphism, F preserves the limit of the empty diagram; equivalently F preserves terminal objects.

Русский

Если терминальное сравнение F изоморфно, F сохраняет предел пустого диаграммы; эквивалентно F сохраняет терминальные объекты.

LaTeX

$$[IsIso (terminalComparison F)] ⇒ PreservesLimit (Functor.empty C) F$$

Lean4

/-- If `terminalComparison F` is an Iso, then `F` preserves terminal objects. -/
theorem preservesLimit_empty_of_isIso_terminalComparison [IsIso (terminalComparison F)] :
    PreservesLimit (Functor.empty.{0} C) F :=
  by
  apply preservesLimit_of_preserves_limit_cone isTerminalTensorUnit
  apply isLimitChangeEmptyCone D isTerminalTensorUnit
  exact asIso (terminalComparison F) |>.symm

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