mk' — Mathlib

English

If for every A,B there exists a cofan c with IsColimit c and Mono c.inl, then there exists a MonoCoprod C.

Русский

Если для любых объектов A,B существует кофан с пределом и моно-Inl, то существует MonoCoprod для всей категории C.

LaTeX

$$$(\\forall A,B). \\exists c\\ (IsColimit c \\land Mono(c.inl)) \\Rightarrow MonoCoprod C$$$

Lean4

theorem mk' (h : ∀ A B : C, ∃ (c : BinaryCofan A B) (_ : IsColimit c), Mono c.inl) : MonoCoprod C :=
  ⟨fun A B c' hc' => by
    obtain ⟨c, hc₁, hc₂⟩ := h A B
    simpa only [mono_inl_iff hc' hc₁] using hc₂⟩

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