op — Mathlib · SciLib

English

If W₁ ≤ W₂ as morphism properties, then for any shape J the induced limitsOfShape satisfy W₁.limitsOfShape J ≤ W₂.limitsOfShape J.

Русский

Если W₁ ≤ W₂ как свойства морфизмов, то для любой формы J получается W₁.limitsOfShape J ≤ W₂.limitsOfShape J.

LaTeX

$$$W_1 \le W_2 \Rightarrow W_1.limitsOfShape J \le W_2.limitsOfShape J \quad(\text{for all } J).$$$

Lean4

instance op [IsStableUnderBaseChange P] : IsStableUnderCobaseChange P.op where
  of_isPushout sq hf := P.of_isPullback sq.unop hf

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