English
If a category has finite products and equalizers, then it has finite limits (same as 69040).
Русский
Если категория имеет конечные произведения и равноселители, то у неё есть конечные пределы.
LaTeX
$$$HasFiniteLimits\,C$$$
Lean4
/-- Any category with finite products and equalizers has all finite limits. -/
@[stacks 002O]
theorem hasFiniteLimits_of_hasEqualizers_and_finite_products [HasFiniteProducts C] [HasEqualizers C] : HasFiniteLimits C
where out _ := { has_limit := fun F => hasLimit_of_equalizer_and_product F }
