compLeftContinuousBounded — Mathlib

English

Left composition by a Lipschitz algebra homomorphism g: β →ₐ[𝕜] γ yields an AlgHom from α →ᵇ β to α →ᵇ γ which preserves algebra structure.

Русский

Левая композиция по гомоморфизму алгебр g: β →ₐ[𝕜] γ даёт AlgHom между пространствами ограниченных функций, сохраняя алгебраическую структуру.

LaTeX

$$$\\text{AlgHom}_{𝕜}(α \\to^b β, α \\to^b γ)$ with compLeftContinuousBounded$$

Lean4

/-- Composition on the left by a (lipschitz-continuous) homomorphism of topological `R`-algebras,
as an `AlgHom`. Similar to `AlgHom.compLeftContinuous`. -/
@[simps!]
protected def compLeftContinuousBounded [NormedRing β] [NormedAlgebra 𝕜 β] [NormedRing γ] [NormedAlgebra 𝕜 γ]
    (g : β →ₐ[𝕜] γ) {C : NNReal} (hg : LipschitzWith C g) : (α →ᵇ β) →ₐ[𝕜] (α →ᵇ γ) :=
  { g.toRingHom.compLeftContinuousBounded α hg with commutes' := fun _ => DFunLike.ext _ _ fun _ => g.commutes' _ }

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