English
If a diagram F: J ⥤ Arrow T has the property that both its left and its right projections F ⋙ leftFunc and F ⋙ rightFunc have limits, then F has a limit in the arrow category Arrow T.
Русский
Если диаграмма F: J ⥤ Arrow T имеет пределы для левых и правых проекций (F ⋙ leftFunc) и (F ⋙ rightFunc), то F имеет предел в категории стрелок Arrow T.
LaTeX
$$$$ \text{HasLimit}(F) \quad \text{whenever} \quad \text{HasLimit}(F \circ \mathrm{leftFunc}) \ \text{and}\ \text{HasLimit}(F \circ \mathrm{rightFunc}). $$$$
Lean4
instance hasLimit (F : J ⥤ Arrow T) [i₁ : HasLimit (F ⋙ leftFunc)] [i₂ : HasLimit (F ⋙ rightFunc)] : HasLimit F :=
by
haveI : HasLimit (F ⋙ Comma.fst _ _) := i₁
haveI : HasLimit (F ⋙ Comma.snd _ _) := i₂
apply Comma.hasLimit
