linearIsometryBoundedOfCompact — Mathlib

English

If α is compact and 𝕜 is a normed field, the 𝕜-algebra of bounded continuous maps α →ᵇ E is 𝕜-linearly isometric to C(α, E).

Русский

Если α компактно и 𝕜 — нормированное поле, то алгебра нормированных ограниченных отображений α →ᵇ E изометрически эквивалентна C(α, E) линейно по отношению к 𝕜.

LaTeX

$$$C(\alpha, E) \cong_{\text{linear isometry}} (α \to^b E)$, i.e. there exists a 𝕜-linear isometry between the two structures.$$

Lean4

/-- When `α` is compact and `𝕜` is a normed field,
the `𝕜`-algebra of bounded continuous maps `α →ᵇ β` is
`𝕜`-linearly isometric to `C(α, β)`.
-/
def linearIsometryBoundedOfCompact : C(α, E) ≃ₗᵢ[𝕜] α →ᵇ E :=
  {
    addEquivBoundedOfCompact α
      E with
    map_smul' := fun c f => by
      ext
      norm_cast
    norm_map' := fun _ => rfl }

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