English
Let ha be a QuasispectrumRestricts a ContinuousMap.realToNNReal. Then for every r ∈ NNReal, the strict inequality relation between quasispectrum in ℝ≥0 and in ℝ is equivalent.
Русский
Пусть ha — QuasispectrumRestricts a ContinuousMap.realToNNReal. Тогда для любого r ∈ NNReal строгие неравенства между квази-спектром ℝ≥0 и спектром ℝ эквивалентны.
LaTeX
$$$\forall r \in \mathbb{R}_{\ge 0},\; (\forall x \in quasispectrum_{\mathbb{R}_{\ge 0}} a, x < r) \iff (\forall x \in quasispectrum_{\mathbb{R}} a, x < r)$$$
Lean4
theorem lt_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]
