English
Let a be an element of a real algebra with a SpectrumRestricts to NNReal. Then for every r ∈ ℝ≥0, the NNReal spectrum of a is bounded above by r exactly when the real spectrum of a is bounded above by r.
Русский
Пусть a принадлежит вещественному алгебраическому пространства; если спектр a ограничен в NNReal, тогда для каждого r ∈ ℝ≥0 множество spectr_ℝ≥0(a) ≤ r эквивалентно тому, что спектр a в ℝ ограничен сверху на r.
LaTeX
$$$\forall r \in \mathbb{R}_{\ge 0},\quad (\forall x \in \mathrm{spectrum}_{\mathbb{R}_{\ge 0}} a, x \le r) \iff (\forall x \in \mathrm{spectrum}_{\mathbb{R}} a, x \le r)$$$
Lean4
theorem nnreal_iff {a : A} : SpectrumRestricts a ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x :=
by
refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
· obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx
exact coe_nonneg x
· exact .of_subset_range_algebraMap (fun _ ↦ Real.toNNReal_coe) fun x hx ↦ ⟨⟨x, h x hx⟩, rfl⟩
