has_limits_of_finite_and_cofiltered

English

Dual to HasColimits_of sizes: if C has finite limits and HasCofilteredLimitsOfSize, then HasLimitsOfSize holds; i.e., all small limits exist.

Русский

Дуал HasColimits_of_sizes: если C имеет конечные пределы и HasCofilteredLimitsOfSize, то HasLimitsOfSize справедливо; то есть существуют малые пределы.

LaTeX

$$$$ \text{has_limits_of_finite_and_cofiltered} \;:\; [HasFiniteLimits\, C] \to [HasCofilteredLimitsOfSize\{w,w\}\, C] \to [HasLimitsOfSize\, C]. $$$$

Lean4

theorem has_limits_of_finite_and_cofiltered [HasFiniteLimits C] [HasCofilteredLimitsOfSize.{w, w} C] :
    HasLimitsOfSize.{w, w} C :=
  have : HasProducts.{w} C := hasProducts_of_finite_and_cofiltered
  has_limits_of_hasEqualizers_and_products

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