spectrum_nonempty

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

URI: https://scilib.ai/kg/mathlib#NNReal.spectrum_nonempty

← MathLib Explorer

English

If a,b ≥ 0 and ab=ba, then 0 ≤ a b.

Русский

Если a,b ≥ 0 и ab=ba, то 0 ≤ ab.

LaTeX

$$$$ a,b \\ge 0 \\land [a,b]=0 \\Rightarrow 0 \\le ab $$$$

Lean4

theorem spectrum_nonempty {A : Type*} [Ring A] [StarRing A] [LE A] [TopologicalSpace A] [Algebra ℝ≥0 A]
    [ContinuousFunctionalCalculus ℝ≥0 A (0 ≤ ·)] [Nontrivial A] {a : A} (ha : 0 ≤ a) : (spectrum ℝ≥0 a).Nonempty :=
  CFC.spectrum_nonempty ℝ≥0 a ha

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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