nnnorm_cfc_le — Mathlib

English

In the NNReal setting with an isometric continuous functional calculus, if f is bounded by c on the spectrum of a, then the NN-norm of cfc f a is bounded by c: ‖cfc f a‖₊ ≤ c.

Русский

В обстановке NNReal при изометрическом непрерывном функциональном калькуляторе, если ‖f(x)‖₊ ≤ c на спектре a, то ‖cfc f a‖₊ ≤ c.

LaTeX

$$$0 \le c \\land \Big( \forall x \in \sigma 𝕜 a, \|f x\|_+ \le c \Big) \Rightarrow \|cfc f a\|_+ \le c$$$

Lean4

theorem nnnorm_cfc_le {f : 𝕜 → 𝕜} {a : A} (c : ℝ≥0) (h : ∀ x ∈ σ 𝕜 a, ‖f x‖₊ ≤ c) : ‖cfc f a‖₊ ≤ c :=
  norm_cfc_le c.2 h

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