spectrum_subset_quasispectrum — Mathlib

English

For any commutative semiring R and algebra A over R, the spectrum of an element a ∈ A is contained in its quasispectrum: spectrum(R, a) ⊆ quasispectrum(R, a).

Русский

Для любой коммутативной полупрямой кольца R и алгебры A над R спектр элемента a ∈ A содержится в его квази-спектре: spectrum(R, a) ⊆ quasispectrum(R, a).

LaTeX

$$$\operatorname{spectrum}(R,a) \subseteq \operatorname{quasispectrum}(R,a)$$$

Lean4

theorem spectrum_subset_quasispectrum (R : Type*) {A : Type*} [CommSemiring R] [Ring A] [Algebra R A] (a : A) :
    spectrum R a ⊆ quasispectrum R a :=
  quasispectrum_eq_spectrum_union R a ▸ Set.subset_union_left

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