instIsSplitEpiR

Mathlib.CategoryTheory.Retract

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Retract.instIsSplitEpiR

English

If h is a retract from X to Y, then h.r is a split epimorphism.

Русский

Если h является развёрткой (retract) X → Y, то h.r является раздвоенным эпиморфизмом.

LaTeX

$$$\mathrm{IsSplitEpi}\; h.r$$$

Lean4

instance : IsSplitEpi h.r :=
  ⟨⟨h.splitEpi⟩⟩

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

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

Разделы

Аффилиация

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