mono_ι

Mathlib.CategoryTheory.Limits.MonoCoprod

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

← MathLib Explorer

English

Another formulation asserting mono of injection at index i under HasCoproduct.

Русский

Другая формулировка утверждает моно инъекции для индекса i под условием HasCoproduct.

LaTeX

$$$Mono\\ (c.inj i)$$$

Lean4

instance mono_ι [HasCoproduct X] (i : I) [HasCoproduct (fun (k : ((Set.range (fun _ : Unit ↦ i))ᶜ : Set I)) => X k.1)] :
    Mono (Sigma.ι X i) :=
  mono_inj X _ (colimit.isColimit _) i

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

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

Разделы

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

Аффилиация

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