English
If a functor F: J → Comma L R has certain limits preserved by R, then F has a limit in the comma category; the cone is built by combining the limits of fst and snd with the preserving functor.
Русский
Если для F: J → Comma L R существуют пределы и пределы сохраняются R, то F имеет предел в коммепии; конус строится сочетанием пределов fst и snd с сохраняющим функтором.
LaTeX
$$$\\text{HasLimit}(F)$ при условии $HasLimit(F \\cdot fst L R)$, $HasLimit(F \\cdot snd L R)$ и $PreservesLimit(F \\cdot snd L R, R)$.$$
Lean4
instance hasLimit (F : J ⥤ Comma L R) [HasLimit (F ⋙ fst L R)] [HasLimit (F ⋙ snd L R)]
[PreservesLimit (F ⋙ snd L R) R] : HasLimit F :=
HasLimit.mk ⟨_, coneOfPreservesIsLimit _ (limit.isLimit _) (limit.isLimit _)⟩
