instIsSplitMonoI

Mathlib.CategoryTheory.Retract

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

English

If h is a retract X → Y, then h.i is a split mono.

Русский

Если h является retract X → Y, то h.i является раздельным моно

LaTeX

$$$\mathrm{IsSplitMono}\; h.i$$$

Lean4

instance : IsSplitMono h.i :=
  ⟨⟨h.splitMono⟩⟩

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

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

Разделы

Аффилиация

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