instIsSplitMonoOppositeOpOfIsSplitEpi

Mathlib.CategoryTheory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsSplitMonoOppositeOpOfIsSplitEpi

English

If f is IsSplitEpi, then f.op is IsSplitMono.

Русский

Если f — раздельное эпиморфизм, то f.op — раздельный мономорфизм.

LaTeX

$$$ [\mathrm{IsSplitEpi}(f)] \Rightarrow \mathrm{IsSplitMono}(f^{\mathrm{op}}).$$$

Lean4

instance [IsSplitEpi f] : IsSplitMono f.op :=
  .mk' IsSplitEpi.exists_splitEpi.some.op

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

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

Разделы

Аффилиация

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