spectrumRestricts

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.spectrumRestricts

English

For self-adjoint a, spectrum of a in real calculus restricts to reals.

Русский

Для самосопряженного a спектр в вещественном калькуляторе ограничивается вещественными числами.

LaTeX

$$$$ \\operatorname{spectrum}(a) \\subset \\mathbb{R} $$$$

Lean4

theorem spectrumRestricts {a : A} (ha : IsSelfAdjoint a) : SpectrumRestricts a Complex.reCLM :=
  ha.quasispectrumRestricts

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru