pushouts_le_iff — Mathlib

English

For any morphism properties P and Q with Q stable under cobase change, P.pushouts ≤ Q if and only if P ≤ Q.

Русский

Для любых свойств P и Q морфизмов, причём Q стабильно по cobase change, выполняется P.pushouts ≤ Q тогда и только тогда P ≤ Q.

LaTeX

$$$[Q.IsStableUnderCobaseChange]\;:\; P.pushouts \le Q \iff P \le Q.$$$

Lean4

@[simp]
theorem pushouts_le_iff {P Q : MorphismProperty C} [Q.IsStableUnderCobaseChange] : P.pushouts ≤ Q ↔ P ≤ Q :=
  by
  constructor
  · exact le_trans P.le_pushouts
  · intro h
    exact le_trans (pushouts_monotone h) pushouts_le

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