hasLimit_of_comp — Mathlib

English

If HasLimit (F ⋙ G), then HasLimit G.

Русский

Если есть предел у F ⋙ G, то есть предел у G.

LaTeX

$$$\\text{HasLimit}(F \\circ G) \\Rightarrow \\text{HasLimit}(G).$$$

Lean4

/-- When `F` is initial, and `F ⋙ G` has a limit, then `G` has a limit also.

We can't make this an instance, because `F` is not determined by the goal.
(Even if this weren't a problem, it would cause a loop with `comp_hasLimit`.)
-/
theorem hasLimit_of_comp [HasLimit (F ⋙ G)] : HasLimit G :=
  HasLimit.mk (limitConeOfComp F (getLimitCone (F ⋙ G)))

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