hasFiniteLimits_of_hasLimits — Mathlib

English

If C has finite limits for all small finite J, then HasLimitsOfShape J C for such J.

Русский

Если в C существуют пределы всех конечных форм для всех малых конечных J, то HasLimitsOfShape J C для таких J.

LaTeX

$$$\forall J\; (\text{Fin}(J) \Rightarrow \operatorname{HasLimitsOfShape}(J, C))$$$

Lean4

/-- If `C` has all limits, it has finite limits. -/
instance (priority := 100) hasFiniteLimits_of_hasLimits [HasLimits C] : HasFiniteLimits C :=
  hasFiniteLimits_of_hasLimitsOfSize C

Похожие утверждения