hasLimitsOfShape_of_isConnected — Mathlib

English

If J is connected and C has limits of shape J, then Over B has limits of shape J.

Русский

Если J связно и C имеет пределы формы J, то Over B имеет пределы формы J.

LaTeX

$$$[IsConnected J] \Rightarrow (\text{HasLimitsOfShape } J (Over B)).$$$

Lean4

/-- The over category has any connected limit which the original category has. -/
instance hasLimitsOfShape_of_isConnected {B : C} [IsConnected J] [HasLimitsOfShape J C] : HasLimitsOfShape J (Over B)
    where has_limit F := hasLimit_of_created F (forget B)

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