isCoseparator_prod_of_isCoseparator_left

English

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

Русский

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

LaTeX

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

Lean4

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

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