pushouts_le — Mathlib

English

If P is stable under cobase change, then for any pushout diagram, the right-hand leg has the property whenever the left-hand leg has it.

Русский

Если P устойчива к cobase change, то в любом диаграмме пуш-аут правая стрелка обладает свойством, когда левая обладает свойством.

LaTeX

$$$[P.IsStableUnderCobaseChange] \Rightarrow P.pushouts \le P.$$$

Lean4

theorem pushouts_le [P.IsStableUnderCobaseChange] : P.pushouts ≤ P := by
  rwa [← isStableUnderCobaseChange_iff_pushouts_le]

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