hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape

English

If F creates limits of shape J and D has limits of shape J, then C has limits of shape J.

Русский

Если F создаёт пределы формы J, а D имеет пределы формы J, то C имеет пределы формы J.

LaTeX

$$$\forall F : C \to D,\ [\text{HasLimitsOfShape } J D] \Rightarrow [\text{CreatesLimitsOfShape } J F] \Rightarrow \text{HasLimitsOfShape } J C$$$

Lean4

/-- If `F` creates limits of shape `J`, and `D` has limits of shape `J`, then
`C` has limits of shape `J`.
-/
theorem hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (F : C ⥤ D) [HasLimitsOfShape J D]
    [CreatesLimitsOfShape J F] : HasLimitsOfShape J C :=
  ⟨fun G => hasLimit_of_created G F⟩

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