comp — Mathlib

English

The composition of two continuous monoid homomorphisms is again a continuous monoid homomorphism.

Русский

Составление двух непрерывных моноид-гомоморфизмов снова даёт непрерывный моноид-гомоморфизм.

LaTeX

$$$g:A\\to_{}^* B$, $f:B\\to_{}^* C$ implies $g\\circ f: A\\to_{}^* C$ is continuous.$$

Lean4

/-- Composition of two continuous homomorphisms. -/
@[to_additive (attr := simps!) /-- Composition of two continuous homomorphisms. -/
    ]
def comp (g : B →ₜ* C) (f : A →ₜ* B) : A →ₜ* C :=
  ⟨g.toMonoidHom.comp f.toMonoidHom, (map_continuous g).comp (map_continuous f)⟩

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