retracts

Mathlib.CategoryTheory.MorphismProperty.Retract

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.retracts

Lean4

/-- The class of morphisms that are retracts of morphisms
belonging to `P : MorphismProperty C`. -/
def retracts (P : MorphismProperty C) : MorphismProperty C := fun _ _ f ↦
  ∃ (Z W : C) (g : Z ⟶ W) (_ : RetractArrow f g), P g

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

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

Разделы

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

Аффилиация

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