le_nnnorm_of_mem_quasispectrum — Mathlib

English

If x ∈ quasispectrum ℝ≥0 a for a nonunital C*-algebra element a, then x ≤ ∥a∥₊.

Русский

Если x принадлежит к квази-спектрумному множеству ℝ≥0 элемента a в неприводимой C*-алгебре, то x не превосходит норму ‖a‖₊.

LaTeX

$$$$x \in \operatorname{quasispectrum}\_{\mathbb{R}_{\ge 0}}(a) \implies x \le \|a\|_{+}.$$$$

Lean4

theorem le_nnnorm_of_mem_quasispectrum {A : Type*} [NonUnitalCStarAlgebra A] {a : A} {x : ℝ≥0}
    (hx : x ∈ quasispectrum ℝ≥0 a) : x ≤ ‖a‖₊ :=
  by
  rw [Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ] at hx
  simpa [Unitization.nnnorm_inr] using spectrum.le_nnnorm_of_mem hx

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