coprod — Mathlib

English

Coproduct of two continuous homomorphisms to the same space is formed by taking the product map alongside multiplication.

Русский

Копрод двух непрерывных гомоморфизмов в одну и ту же цель формируется через произведение и умножение.

LaTeX

$$$coprod(f:g) = (mul_E).\\,comp\\, (f.prodMap g)$$$

Lean4

/-- Coproduct of two continuous homomorphisms to the same space. -/
@[to_additive (attr := simps!) /-- Coproduct of two continuous homomorphisms to the same space. -/
    ]
def coprod (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) : ContinuousMonoidHom (A × B) E :=
  (mul E).comp (f.prodMap g)

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