instCStarRing — Mathlib

English

There is a star-algebra homomorphism forgetting that a bounded continuous function is bounded, mapping into a suitable algebra of continuous maps.

Русский

Существуют звёздно-алгебра-хомоморфизмы, переводящие ограниченно непрерывную функцию в соответствующую алгебру непрерывных отображений.

LaTeX

$$$$\text{toContinuousMapStar}_\mathbb{K}: (\alpha \to^b \beta) \to_{\text{StarAlg}} C(\alpha, \beta).$$$$

Lean4

instance instCStarRing : CStarRing (α →ᵇ β) where
  norm_mul_self_le
    f := by
    rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), norm_le (Real.sqrt_nonneg _)]
    intro x
    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
    exact norm_coe_le_norm (star f * f) x

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