English
If G preserves equalizers and finite products, then it preserves finite limits.
Русский
Если G сохраняет равноселители и конечные произведения, то он сохраняет конечные пределы.
LaTeX
$$[HasEqualizers C] [HasFiniteProducts C] ⇒ PreservesFiniteLimits G$$
Lean4
/-- If G preserves equalizers and finite products, it preserves finite limits. -/
theorem preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts [HasEqualizers C] [HasFiniteProducts C]
(G : C ⥤ D) [PreservesLimitsOfShape WalkingParallelPair G] [PreservesFiniteProducts G] : PreservesFiniteLimits G
where
preservesFiniteLimits := by
intros
apply preservesLimit_of_preservesEqualizers_and_product
