preservesLimitsOfShape_pempty_of_preservesTerminal

English

Preserving the terminal object implies preserving all limits of the empty diagram.

Русский

Сохранение терминального объекта подразумевает сохранение всех пределов пустой диаграммы.

LaTeX

$$$[\\text{PreservesLimit}(\\mathrm{Functor.empty}, G)] \\Rightarrow \\text{PreservesLimitsOfShape}(\\mathrm{Discrete} \\mathrm{PEmpty}, G).$$$

Lean4

/-- Preserving the terminal object implies preserving all limits of the empty diagram. -/
theorem preservesLimitsOfShape_pempty_of_preservesTerminal [PreservesLimit (Functor.empty.{0} C) G] :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) G where
  preservesLimit := preservesLimit_of_iso_diagram G (Functor.emptyExt (Functor.empty.{0} C) _)

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