instIsStableUnderRetractsRetractClosure

English

The operator retractClosure preserves retracts: retractClosure(P) is stable under retracts.

Русский

Оператор retractClosure сохраняет ретракты: retractClosure(P) сохраняется под ретракциями.

LaTeX

$$IsStableUnderRetracts(\operatorname{retractClosure}(P))$$

Lean4

instance : IsStableUnderRetracts (retractClosure P) where
  of_retract := by
    rintro X Y r₁ ⟨Z, hZ, ⟨r₂⟩⟩
    refine ⟨Z, hZ, ⟨r₁.trans r₂⟩⟩

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