mono_binaryCofanSum_inl

Mathlib.CategoryTheory.Limits.MonoCoprod

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl

← MathLib Explorer

English

The left leg of binaryCofanSum is mono

Русский

Левая ножка binaryCofanSum моно

LaTeX

$$[MonoCoprod C] ⇒ Mono((binaryCofanSum c c1 c2 hc1 hc2).inl)$$

Lean4

theorem mono_binaryCofanSum_inl [MonoCoprod C] : Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl :=
  MonoCoprod.binaryCofan_inl _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

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

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

Разделы

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

Аффилиация

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