hasLimitsOfSize — Mathlib

English

If Over X has limits of size w, w', then Subobject X has limits of size w, w'.

Русский

Если Over X имеет пределы размера w, w', то Subobject X имеет пределы размера w, w'.

LaTeX

$$$\mathrm{HasLimitsOfSize}^{(w, w')} (\mathrm{Over} X) \Rightarrow \mathrm{HasLimitsOfSize}^{(w, w')} (\mathrm{Subobject} X)$$$

Lean4

instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} (Over X)] : HasLimitsOfSize.{w, w'} (Subobject X) where
  has_limits_of_shape _ _ := by infer_instance

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