isSplitMono_from

Mathlib.CategoryTheory.Limits.Shapes.Terminal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.terminal.isSplitMono_from

← MathLib Explorer

English

Any morphism from a terminal object is split mono.

Русский

Любой морфизм из терминального объекта является разделенным моно.

LaTeX

$$$\\text{IsSplitMono}(f) \\quad\\text{for } f: 1 \\to Y$$$

Lean4

/-- Any morphism from a terminal object is split mono. -/
instance isSplitMono_from {Y : C} [HasTerminal C] (f : ⊤_ C ⟶ Y) : IsSplitMono f :=
  IsTerminal.isSplitMono_from terminalIsTerminal _

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

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

Разделы

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

Аффилиация

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