nnnorm_cfcₙ_lt — Mathlib

English

If on the spectrum of a, f x < c holds for all x, then ‖cfcₙ f a‖₊ < c.

Русский

Если на спектре a выполняется f x < c для всех x, то ‖cfcₙ f a‖₊ < c.

LaTeX

$$$\forall x \in \sigma_n ℝ≥0 a, \; ‖f x‖_+ < c \Rightarrow ‖cfc_n f a‖_+ < c$$$

Lean4

theorem nnnorm_cfcₙ_lt {f : 𝕜 → 𝕜} {a : A} {c : ℝ≥0} (h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ < c) : ‖cfcₙ f a‖₊ < c :=
  norm_cfcₙ_lt h

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