hasLimitsOfSize — Mathlib

English

If Over X has limits of size {w,w'}, then MonoOver X has limits of size {w,w'}.

Русский

Если Over X имеет пределы размера {w, w'}, то MonoOver X имеет пределы того же размера.

LaTeX

$$HasLimitsOfSize.{w, w'} (Over X) ⇒ HasLimitsOfSize.{w, w'} (MonoOver X)$$

Lean4

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

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