nonneg_of_mem_quasispectrum — Mathlib

English

If a ≥ 0 and x ∈ quasispectrum 𝕜 a, then x ≥ 0.

Русский

Если a ≥ 0 и x ∈ quasispectrum 𝕜 a, то x ≥ 0.

LaTeX

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

Lean4

theorem nonneg_of_mem_quasispectrum {𝕜 : Type*} [CommSemiring 𝕜] [PartialOrder 𝕜] [PartialOrder A] [Module 𝕜 A]
    [NonnegSpectrumClass 𝕜 A] {a : A} (ha : 0 ≤ a) {x : 𝕜} (hx : x ∈ quasispectrum 𝕜 a) : 0 ≤ x :=
  quasispectrum_nonneg_of_nonneg a ha x hx

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