of_coproductDisjoint — Mathlib

English

If a colimit of a coproduct diagram X is given, then each injection c.inj i is mono, i.e., the canonical injections from the coproduct are monomorphisms.

Русский

Если существует колимит coproduct-диаграммы для X, то каждое внедрение инъекции из сопряженного coproduct является моно.

LaTeX

$$$\\text{Mono}\\,(c.inj\\ i)$$$

Lean4

theorem _root_.CategoryTheory.Mono.of_coproductDisjoint {c : Cofan X} (hc : IsColimit c) (i : ι) : Mono (c.inj i) :=
  CoproductDisjoint.mono_inj hc i

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