mono_of_injective — Mathlib

English

Under HasCoproduct and related conditions, the map Cofan.IsColimit.desc hc1 (fun i => c.inj (ι i)) is mono.

Русский

При условии существования копроодукта и т.д. отображение описания десса моно.

LaTeX

$$$Mono\\ (Cofan.IsColimit.desc\\ hc_1\\ (\\lambda i. c.inj (ι i))).$$$

Lean4

theorem mono_of_injective [HasCoproduct (fun (k : ((Set.range ι)ᶜ : Set I)) => X k.1)] :
    Mono (Cofan.IsColimit.desc hc₁ (fun i => c.inj (ι i))) :=
  mono_of_injective_aux X ι hι c c₁ hc hc₁ _ (colimit.isColimit _)

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