spectrum_pos — Mathlib

English

If a is strictly positive, then every spectral value x of a (in 𝕜) is positive: x > 0.

Русский

Если a строго положительно, то каждый спектральный элемент x в спектре a положителен: x > 0.

LaTeX

$$∀ x ∈ spectrum 𝕜 a, 0 < x$$

Lean4

theorem spectrum_pos [CommSemiring 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] {a : A}
    (ha : IsStrictlyPositive a) {x : 𝕜} (hx : x ∈ spectrum 𝕜 a) : 0 < x :=
  by
  have h₁ : 0 ≤ x := by grind
  have h₂ : x ≠ 0 := by grind [= spectrum.zero_notMem_iff]
  exact lt_of_le_of_ne h₁ h₂.symm

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