retracts_le_iff — Mathlib

English

Let P and Q be morphism properties with Q stable under retracts. Then P.retracts ≤ Q iff P ≤ Q.

Русский

Пусть P и Q — свойства морфизмов, причём Q стабилен под retracts. Тогда P.retracts ≤ Q тогда и только тогда, когда P ≤ Q.

LaTeX

$$$(P.retracts \le Q) \iff (P \le Q)$, при [Q.IsStableUnderRetracts]$$

Lean4

@[simp]
theorem retracts_le_iff {P Q : MorphismProperty C} [Q.IsStableUnderRetracts] : P.retracts ≤ Q ↔ P ≤ Q :=
  by
  constructor
  · exact le_trans P.le_retracts
  · intro h
    exact le_trans (retracts_monotone h) Q.retracts_le

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