spectrum_nonneg_of_nonneg — Mathlib

English

If a ≥ 0, then every x ∈ spectrum 𝕜 a satisfies x ≥ 0.

Русский

Если a ≥ 0, то для каждого x ∈ spectrum 𝕜 a верно x ≥ 0.

LaTeX

$$0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x$$

Lean4

theorem spectrum_nonneg_of_nonneg {𝕜 A : Type*} [CommSemiring 𝕜] [PartialOrder 𝕜] [Ring A] [PartialOrder A]
    [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] ⦃a : A⦄ (ha : 0 ≤ a) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) : 0 ≤ x :=
  NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg a ha x (spectrum_subset_quasispectrum 𝕜 a hx)

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