nnreal_lt_iff — Mathlib

English

Under a SpectrumRestricts a realToNNReal, for any r ∈ ℝ≥0, the strict inequality ∀ x ∈ spectrum NNReal a, x < r iff ∀ x ∈ spectrum Real a, x < r holds.

Русский

При наличии 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 < r) \iff (\forall x \in spectrum_{\mathbb{R}} a, x < r)$$$

Lean4

theorem nnreal_lt_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]

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