English
Right composition by a continuous map g: C(α, β) → C(α, γ) given by f ↦ f ∘ g defines a MonoidHom from C(β, γ) to C(α, γ).
Русский
Правая композиция по непрерывному отображению g: C(α, β) → C(α, γ) задаёт моноидгомомorphism: f ↦ f ∘ g.
LaTeX
$$$\forall g:\; C(α, β) \to C(α, γ),\; f\mapsto f\circ g,\; \text{MonoidHom}_{β\to γ}\to(α\to γ)$$$
Lean4
/-- Composition on the right as a `MonoidHom`. Similar to `MonoidHom.compHom'`. -/
@[to_additive (attr := simps) /-- Composition on the right as an `AddMonoidHom`. Similar to `AddMonoidHom.compHom'`. -/
]
def compMonoidHom' {γ : Type*} [TopologicalSpace γ] [MulOneClass γ] [ContinuousMul γ] (g : C(α, β)) : C(β, γ) →* C(α, γ)
where
toFun f := f.comp g
map_one' := one_comp g
map_mul' f₁ f₂ := mul_comp f₁ f₂ g
