English
If G preserves equalizers and products, it preserves all limits.
Русский
Если G сохраняет равноселители и произведения, он сохраняет все пределы.
LaTeX
$$PreservesLimitsOfShape WalkingParallelPair G$$
Lean4
/-- If G preserves equalizers and products, it preserves all limits. -/
theorem preservesLimits_of_preservesEqualizers_and_products [HasEqualizers C] [HasProducts.{w} C] (G : C ⥤ D)
[PreservesLimitsOfShape WalkingParallelPair G] [∀ J, PreservesLimitsOfShape (Discrete.{w} J) G] :
PreservesLimitsOfSize.{w, w} G where preservesLimitsOfShape := preservesLimit_of_preservesEqualizers_and_product G
