prod — Mathlib

English

The product of two continuous monoid homomorphisms on the same domain is a continuous monoid homomorphism into the product codomain.

Русский

Произведение двух непрерывных моноид-гомоморфизмов на одной области — это непрерывный моноид-гомоморфизм в произведение кодом.

LaTeX

$$$f:A\\to_* B$, $g:A\\to_* C$ and then $f.prod\,g: A\\to_* (B×C)$$$

Lean4

/-- Product of two continuous homomorphisms on the same space. -/
@[to_additive (attr := simps!) prod /-- Product of two continuous homomorphisms on the same space. -/
    ]
def prod (f : A →ₜ* B) (g : A →ₜ* C) : A →ₜ* (B × C) :=
  ⟨f.toMonoidHom.prod g.toMonoidHom, f.continuous_toFun.prodMk g.continuous_toFun⟩

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