English
Left composition by a Lipschitz continuous monoid homomorphism g: β → γ yields a MonoidHom from α →ᵇ β to α →ᵇ γ, preserving multiplication and identity.
Русский
Левая композиция с Lipschitz-постоянной моноид-гомоморфизмом g: β → γ задаёт моноид-гомоморфизм между α →ᵇ β и α →ᵇ γ, сохраняющий умножение и единицу.
LaTeX
$$$\text{compLeftContinuousBounded}(g, hg): (α \to^{\mathrm{b}} β) \to* (α \to^{\mathrm{b}} γ)$ is a MonoidHom with $\bigl( f \mapsto f \circ g \bigr)$$$
Lean4
/-- Composition on the left by a (lipschitz-continuous) homomorphism of topological monoids, as a
`MonoidHom`. Similar to `MonoidHom.compLeftContinuous`. -/
@[to_additive (attr := simps) /--
Composition on the left by a (lipschitz-continuous) homomorphism of topological `AddMonoid`s,
as a `AddMonoidHom`. Similar to `AddMonoidHom.compLeftContinuous`. -/
]
protected def _root_.MonoidHom.compLeftContinuousBounded (α : Type*) [TopologicalSpace α] [PseudoMetricSpace β]
[Monoid β] [BoundedMul β] [ContinuousMul β] [PseudoMetricSpace γ] [Monoid γ] [BoundedMul γ] [ContinuousMul γ]
(g : β →* γ) {C : NNReal} (hg : LipschitzWith C g) : (α →ᵇ β) →* (α →ᵇ γ)
where
toFun f := f.comp g hg
map_one' := ext fun _ => g.map_one
map_mul' _ _ := ext fun _ => g.map_mul _ _
