mono_inr_of_isColimit — Mathlib

English

In a finitely extensive category, mono-inr of a colimit cofan is mono.

Русский

В конечносильно-разложимой категории моно-правило Inr является моно.

LaTeX

$$$\forall C, \forall X,Y, \forall c: BinaryCofan X Y, \text{IsColimit}(c) \Rightarrow \text{Mono}(c.\mathrm{inr})$$$

Lean4

theorem mono_inr_of_isColimit [FinitaryExtensive C] {c : BinaryCofan X Y} (hc : IsColimit c) : Mono c.inr :=
  BinaryCofan.mono_inr_of_isVanKampen (FinitaryExtensive.vanKampen c hc)

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