hasLimits_of_hasLimits_createsLimits

English

If F creates limits and D has all limits, then C has all limits.

Русский

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

LaTeX

$$$\forall F : C \to D\, [\text{CreatesLimitsOfSize } F] \wedge [\text{HasLimitsOfSize } D] \Rightarrow [\text{HasLimitsOfSize } C]$$$

Lean4

/-- If `F` creates limits, and `D` has all limits, then `C` has all limits. -/
theorem hasLimits_of_hasLimits_createsLimits (F : C ⥤ D) [HasLimitsOfSize.{w, w'} D] [CreatesLimitsOfSize.{w, w'} F] :
    HasLimitsOfSize.{w, w'} C :=
  ⟨fun _ _ => hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape F⟩
    -- Interface to the `CreatesColimit` class.

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