CategoryTheory.Limits.initialMonoClass_of_disjoint_coproducts

theorem CategoryTheory.Limits.initialMonoClass_of_disjoint_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.CoproductsDisjoint C], CategoryTheory.Limits.InitialMonoClass C

This theorem states that in any category `C` that has disjoint coproducts, any morphism originating from an initial object is a monomorphism. It's worth noting that it's not necessarily the case that `C` has strict initial objects. An example of this can be seen in the category of types and partial functions.

More concisely: In any category with disjoint coproducts, morphisms from the initial object are monomorphisms.