English
Let A be a ring with a real algebra structure. If the spectrum of a element a in A, when viewed inside NNReal (through real-to-NNReal), is contained in the interval [0, r], then the spectrum of a considered in the real spectrum is also contained in [0, r]; in other words, restricting the spectrum to NNReal does not enlarge upper bounds.
Русский
Пусть A — кольцо с вещественным алгебраическим строением. Если спектр элемента a в A, рассмотренный через преобразование Real → ℝ≥0, лежит в промежутке [0, r], то спектр a в действительном спектре также лежит в [0, r]. Иными словами, ограничение спектра до NNReal не увеличивает верхнюю границу.
LaTeX
$$$(\forall x \in spectrum \; \mathbb{R}_{\ge 0} a, x \le r) \iff (\forall x \in spectrum \; a, x \le r)$$$
Lean4
theorem le_nnreal_iff {a : A} (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
(∀ x ∈ spectrum ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ spectrum ℝ a, x ≤ r := by simp [← ha.algebraMap_image]
