retractClosure_eq_self

Mathlib.CategoryTheory.ObjectProperty.Retract

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.retractClosure_eq_self

← MathLib Explorer

English

If P is stable under retracts, then retractClosure P = P.

Русский

Если P устойчиво к ретракциям, то retractClosure(P) = P.

LaTeX

$$$[\text{IsStableUnderRetracts}(P)] \Rightarrow \operatorname{retractClosure}(P) = P$$$

Lean4

theorem retractClosure_eq_self [IsStableUnderRetracts P] : retractClosure P = P :=
  by
  apply le_antisymm
  · intro X ⟨Y, hY, ⟨e⟩⟩
    exact prop_of_retract P e hY
  · exact le_retractClosure P

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru