instHasLimitsOfShapeOverOfWithTerminal

English

If liftFromOver.obj F has a limit, then F has a limit in the over category Over X.

Русский

Если у obj F из liftFromOver существует предел, то F имеет предел в категории Over X.

LaTeX

$$$\forall X\, (F : J \to \mathrm{Over} X),\ [\mathrm{HasLimit} (\mathrm{liftFromOver.obj} F)] \Rightarrow \mathrm{HasLimit} F$$$

Lean4

instance (X : C) [HasLimitsOfShape (WithTerminal J) C] : HasLimitsOfShape J (Over X) where
  has_limit _ := Over.hasLimit_of_hasLimit_liftFromOver ..

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