le_retracts

Mathlib.CategoryTheory.MorphismProperty.Retract

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

English

For any W, W ≤ W.retracts.

Русский

Для любого W выполняется W ≤ W.retracts.

LaTeX

$$W \le W.retracts$$

Lean4

theorem le_retracts (P : MorphismProperty C) : P ≤ P.retracts :=
  by
  intro X Y f hf
  exact ⟨_, _, f, { i := 𝟙 _, r := 𝟙 _ }, hf⟩

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

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

Разделы

Аффилиация

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