English
Left composition by a continuous monoid hom g: β →* γ induces a MonoidHom from C(α, β) to C(α, γ), by f ↦ g ∘ f.
Русский
Левая композиция устойчиво задаёт моноидный морфизм: f ↦ g ∘ f, где g: β →* γ непрерывен.
LaTeX
$$$\forall g:\, C(α, β)\to C(α, γ),\; f\mapsto g\circ f,\; (g,\,f)\mapsto g\circ f$$$
Lean4
/-- Composition on the left by a (continuous) homomorphism of topological monoids, as a
`MonoidHom`. Similar to `MonoidHom.compLeft`. -/
@[to_additive (attr := simps) /--
Composition on the left by a (continuous) homomorphism of topological `AddMonoid`s, as an
`AddMonoidHom`. Similar to `AddMonoidHom.comp_left`. -/
]
protected def _root_.MonoidHom.compLeftContinuous {γ : Type*} [Monoid β] [ContinuousMul β] [TopologicalSpace γ]
[Monoid γ] [ContinuousMul γ] (g : β →* γ) (hg : Continuous g) : C(α, β) →* C(α, γ)
where
toFun f := (⟨g, hg⟩ : C(β, γ)).comp f
map_one' := ext fun _ => g.map_one
map_mul' _ _ := ext fun _ => g.map_mul _ _
