mono_binaryCofanSum_inr

Mathlib.CategoryTheory.Limits.MonoCoprod

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

← MathLib Explorer

English

The right leg of binaryCofanSum is mono

Русский

Правая ножка binaryCofanSum моно

LaTeX

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

Lean4

theorem mono_binaryCofanSum_inr [MonoCoprod C] : Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr :=
  MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

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

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

Разделы

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

Аффилиация

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