norm_apply_le_self_mul_norm_one — Mathlib

English

For AlgHom f : A →𝕜 and a ∈ A, the operator norm satisfies ‖f(a)‖ ≤ ‖a‖ · ‖1‖ (in particular ≤ ‖a‖ if ‖1‖ = 1).

Русский

Для алгебраического гомоморфизма f и элемента a спектральная норма удовлетворяет неравенству: ‖f(a)‖ ≤ ‖a‖ · ‖1‖ (а значит ≤ ‖a‖, если ‖1‖ = 1).

LaTeX

$$$\\|f(a)\\| \\le \\|a\\| \\cdot \\|1_A\\|$$$

Lean4

theorem norm_apply_le_self_mul_norm_one [FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] (f : F) (a : A) :
    ‖f a‖ ≤ ‖a‖ * ‖(1 : A)‖ :=
  spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum f _)

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