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