isCoseparator_prod_of_isCoseparator_right

English

If H is a coseparator, then the product G ⨯ H is a coseparator.

Русский

Если H — косепаратор, то произведение G ⨯ H является косепаратором.

LaTeX

$$$\\mathrm{IsCoseparator}(H) \\Rightarrow \\mathrm{IsCoseparator}(G \\times H)$$$

Lean4

theorem isCoseparator_prod_of_isCoseparator_right (G H : C) [HasBinaryProduct G H] (hH : IsCoseparator H) :
    IsCoseparator (G ⨯ H) :=
  (isCoseparator_prod _ _).2 <| IsCoseparating.mono hH <| by simp

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