English
Let α be a topological space and g: β → γ be a Lipschitz, ring-homomorphic map. The operation of composing on the left with g induces a ring homomorphism from the bounded continuous functions α →ᵇ β to α →ᵇ γ, f ↦ g ∘ f.
Русский
Пусть α — топологическое пространство, а g: β → γ — липшицевое кольцевомоморфизм. Операция композиции слева с g порождает кольтовый гомоморфизм от ограниченных непрерывных функций α →ᵇ β к α →ᵇ γ, f ↦ g ∘ f.
LaTeX
$$$\\operatorname{CompLeft}_α(g): (α \\to^b β) \\to^+* (α \\to^b γ)$, $(\\operatorname{CompLeft}_α(g))(f)=g\\circ f$; in particular it is a RingHom.$$
Lean4
/-- Composition on the left by a (lipschitz-continuous) homomorphism of topological semirings, as a
`RingHom`. Similar to `RingHom.compLeftContinuous`. -/
@[simps!]
protected def _root_.RingHom.compLeftContinuousBounded (α : Type*) [TopologicalSpace α] [SeminormedRing β]
[SeminormedRing γ] (g : β →+* γ) {C : NNReal} (hg : LipschitzWith C g) : (α →ᵇ β) →+* (α →ᵇ γ) :=
{ g.toMonoidHom.compLeftContinuousBounded α hg, g.toAddMonoidHom.compLeftContinuousBounded α hg with }
