The coproduct of a separating family of objects is separating

If a family of objects S : ι → C in a category with zero morphisms is separating, then the coproduct of S is a separator in C.

theorem CategoryTheory.IsSeparating.isSeparator_of_isColimit_cofan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type w} {S : ι → C} (hS : CategoryTheory.IsSeparating (Set.range S)) {c : CategoryTheory.Limits.Cofan S} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.IsSeparator c.pt

theorem CategoryTheory.IsSeparating.isSeparator_coproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type w} {S : ι → C} (hS : CategoryTheory.IsSeparating (Set.range S)) [CategoryTheory.Limits.HasCoproduct S] : CategoryTheory.IsSeparator (∐ S)