retracts_le — Mathlib

English

If a morphism property P is stable under retracts, then every retract of a morphism with P also has property P; i.e., retracts(P) ⊆ P.

Русский

Если свойство P устойчиво к retracts, то каждый retract(morphisms with P) тоже обладает свойством P; то есть retracts(P) ⊆ P.

LaTeX

$$$P^{\text{IsStableUnderRetracts}} \Rightarrow \operatorname{retracts}(P) \le P$$$

Lean4

theorem retracts_le (P : MorphismProperty C) [P.IsStableUnderRetracts] : P.retracts ≤ P := by
  rwa [← isStableUnderRetracts_iff_retracts_le]

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