nnreal_of_nonneg — Mathlib

English

If a is nonnegative (ha: 0 ≤ a) in a nonunital ring with module structure over ℝ, then QuasispectrumRestricts a realToNNReal.

Русский

Если a неотрицательно в неединональном кольце с модулем над ℝ, тогда QuasispectrumRestricts a realToNNReal.

LaTeX

$$$\text{QuasispectrumRestricts}(a,\text{realToNNReal})$$$

Lean4

theorem nnreal_of_nonneg [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A]
    [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) : QuasispectrumRestricts a ContinuousMap.realToNNReal :=
  nnreal_iff.mpr <| quasispectrum_nonneg_of_nonneg _ ha

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