quasispectrumRestricts — Mathlib

English

A self-adjoint element has its complex quasispectrum contained in the real line.

Русский

У самосопряженного элемента комплексный квазиспектр ограничен вещественной осью.

LaTeX

$$$$ \\text{QuasispectrumRestricts}(a, \\mathbb{C}\\text{-re}) $$$$

Lean4

theorem quasispectrumRestricts {a : A} (ha : IsSelfAdjoint a) : QuasispectrumRestricts a Complex.reCLM :=
  isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts |>.mp ha |>.2

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