overPost — Mathlib

English

If F preserves limits of a given size, then Over.post F preserves limits of the same size shape.

Русский

Если F сохраняет пределы заданного размера, то и Over.post F сохраняет пределы того же размера формы.

LaTeX

$$$\text{PreservesLimitsOfSize}.{w',w} F \Rightarrow \text{PreservesLimitsOfSize}.{w',w}(\mathrm{Over.post}\ F)$$$

Lean4

instance overPost [PreservesFiniteLimits F] : PreservesFiniteLimits (Over.post F (X := X)) where
  preservesFiniteLimits _ := inferInstance

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