norm_le_norm_one — Mathlib

English

For φ in the character space of a normed algebra, the operator norm of its image in the strong dual is at most the norm of the identity element 1 of the algebra.

Русский

Для φ в пространстве характеров нормированной алгебры операторная норма изображения в сильном двойственном не превосходит нормы единицы 1 в алгебре.

LaTeX

$$$\|\mathrm{toStrongDual}(\phi)\| \leq \|1\|$$$

Lean4

theorem norm_le_norm_one (φ : characterSpace 𝕜 A) : ‖toStrongDual (φ : WeakDual 𝕜 A)‖ ≤ ‖(1 : A)‖ :=
  ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg (1 : A)) fun a =>
    mul_comm ‖a‖ ‖(1 : A)‖ ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ a)

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