isStableUnderRetracts_iff_retracts_le

English

For a morphism property P, stability under retracts is equivalent to the inclusion of retracts into P: P.IsStableUnderRetracts iff P.retracts ≤ P.

Русский

Для свойства P устойчивость к retracts эквивалентна включению retracts в P: P.IsStableUnderRetracts ⇔ P.retracts ≤ P.

LaTeX

$$$P^{\text{IsStableUnderRetracts}} \iff P.retracts \le P$$$

Lean4

theorem isStableUnderRetracts_iff_retracts_le (P : MorphismProperty C) : P.IsStableUnderRetracts ↔ P.retracts ≤ P :=
  by
  rw [isStableUnderRetracts_iff]
  constructor
  · intro h₁ X Y f ⟨_, _, _, h₂, h₃⟩
    exact h₁ h₂ h₃
  · intro h₁ _ _ _ _ _ _ h₂ h₃
    exact h₁ _ ⟨_, _, _, h₂, h₃⟩

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