isSeparator_coprod_of_isSeparator_left

English

If G is a separator, then coprod G H is a separator for any object H, assuming coproduct exists.

Русский

Если G — разделитель, то coprod G H является разделителем для любого H при условии существования копроуда.

LaTeX

$$$\\mathrm{IsSeparator}(G) \\Rightarrow \\mathrm{IsSeparator}(\\mathrm{coprod}\\, G\\, H)$$$

Lean4

theorem isSeparator_coprod_of_isSeparator_left (G H : C) [HasBinaryCoproduct G H] (hG : IsSeparator G) :
    IsSeparator (G ⨿ H) :=
  (isSeparator_coprod _ _).2 <| IsSeparating.mono hG <| by simp

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