hasColimitsOfSize — Mathlib

English

If Over X has colimits of size w, w' (i.e., HasColimitsOfSize (Over X)), then Subobject X has colimits of size w, w' (HasColimitsOfSize (Subobject X)).

Русский

Если Over X имеет конические пределы размера w, w' (HasColimitsOfSize (Over X)), то Subobject X имеет конические пределы размера w, w'.

LaTeX

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

Lean4

instance hasColimitsOfSize : HasColimitsOfSize.{w, w'} (Subobject X) := by apply hasColimitsOfSize_thinSkeleton

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