nnreal_le_iff — Mathlib

English

Let ha be a SpectrumRestricts a realToNNReal. Then for every r ∈ ℝ≥0, the spectrum inequality holds: ∀ x ∈ spectrum NNReal a, x ≤ r iff ∀ x ∈ spectrum Real a, x ≤ r.

Русский

Пусть ha — SpectrumRestricts a realToNNReal. Тогда для любого r ∈ ℝ≥0 выполнено: ∀ x ∈ spectrum NNReal a, x ≤ r эквивалентно ∀ x ∈ spectrum Real a, x ≤ r.

LaTeX

$$$\forall r \in \mathbb{R}_{\ge 0},\; (\forall x \in spectrum_{\mathbb{R}_{\ge 0}} a, x \le r) \iff (\forall x \in spectrum_{\mathbb{R}} a, x \le r)$$$

Lean4

theorem nnreal_le_iff {a : A} (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
    (∀ x ∈ spectrum ℝ≥0 a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, r ≤ x := by simp [← ha.algebraMap_image]

Похожие утверждения