English
Let ha be a QuasispectrumRestricts a ContinuousMap.realToNNReal. Then for every r ∈ ℝ≥0, the same inequality comparing quasispectrum in ℝ≥0 and in ℝ holds: ∀ x ∈ quasispectrum ℝ≥0 a, x ≤ r iff ∀ x ∈ quasispectrum ℝ a, x ≤ r.
Русский
Пусть ha — QuasispectrumRestricts a ContinuousMap.realToNNReal. Тогда для любого r ∈ ℝ≥0 верно то же неравенство, сопоставляющее квазіспектр ℝ≥0 и спектр ℝ: ∀ x ∈ quasispectrum ℝ≥0 a, x ≤ r ⇔ ∀ x ∈ quasispectrum ℝ a, x ≤ r.
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 lt_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]
