English
Let ha be a QuasispectrumRestricts a ContinuousMap.realToNNReal. Then the llg inequality with ≤ is equivalent between quasispectrum ℝ≥0 a and quasispectrum ℝ a for all r.
Русский
Пусть ha — QuasispectrumRestricts a ContinuousMap.realToNNReal. Тогда для всех r верна эквивалентность для неравенств ≤ между квази-спектром ℝ≥0 a и спектром ℝ a.
LaTeX
$$$\forall r \in \mathbb{R}_{\ge 0},\; (\forall x \in quasispectrum_{\mathbb{R}_{\ge 0}} a, x \le r) \iff (\forall x \in quasispectrum_{\mathbb{R}} a, x \le r)$$$
Lean4
theorem nnreal_iff [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} :
QuasispectrumRestricts a ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x := by
rw [quasispectrumRestricts_iff_spectrumRestricts_inr, Unitization.quasispectrum_eq_spectrum_inr' _ ℝ,
SpectrumRestricts.nnreal_iff]
