underPost — Mathlib

English

If F preserves colimits of a certain size, then Under.post F preserves colimits of that size.

Русский

Если F сохраняет колимиты заданного размера, то Under.post F сохраняет колимиты этого размера.

LaTeX

$$$\text{PreservesColimitsOfSize } {w',w} F \Rightarrow \text{PreservesColimitsOfSize } {w',w} (\mathrm{Under.post} F)$$$

Lean4

instance underPost [PreservesColimitsOfSize.{w', w} F] : PreservesColimitsOfSize.{w', w} (Under.post F (X := X)) where

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