hasLimit_of_created — Mathlib

English

If F creates the limit of K and K ⋙ F has a limit, then K has a limit.

Русский

Если F создаёт предел для K, и K ⋙ F имеет предел, то K имеет предел.

LaTeX

$$$\forall K : J \to C,\ F : C \to D\, [\text{CreatesLimit } K F] \wedge [\text{HasLimit } (K \circ F)] \Rightarrow \text{HasLimit } K$$$

Lean4

/-- If `F` creates the limit of `K` and `K ⋙ F` has a limit, then `K` has a limit. -/
theorem hasLimit_of_created (K : J ⥤ C) (F : C ⥤ D) [HasLimit (K ⋙ F)] [CreatesLimit K F] : HasLimit K :=
  HasLimit.mk
    { cone := liftLimit (limit.isLimit (K ⋙ F))
      isLimit := liftedLimitIsLimit _ }

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