isSeparator_coprod_of_isSeparator_right

English

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

Русский

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

LaTeX

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

Lean4

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

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