overPost — Mathlib

English

With PreservesLimitsOfSize for F, Over.post F preserves limits of shape J of that size.

Русский

С PreservesLimitsOfSize для F, Over.post F сохраняет пределы формы J заданного размера.

LaTeX

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

Lean4

instance overPost [PreservesLimitsOfSize.{w', w} F] : PreservesLimitsOfSize.{w', w} (Over.post F (X := X)) where

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