English
Let ha be a QuasispectrumRestricts a ContinuousMap.realToNNReal. Then for any r ∈ NNReal, the inequality over quasispectrum with ≤ holds equivalently for spectra over Real.
Русский
Пусть ha — QuasispectrumRestricts a ContinuousMap.realToNNReal. Тогда для любого r ∈ NNReal неравенство ≤ для квази-спектра эквивалентно неравенству ≤ для спектра над Real.
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 le_nnreal_iff [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A}
(ha : QuasispectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
(∀ x ∈ quasispectrum ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ quasispectrum ℝ a, x ≤ r := by simp [← ha.algebraMap_image]
