nnreal_of_nonneg — Mathlib

English

If a is nonnegative (0 ≤ a) and the spectrum class is NonnegSpectrumClass Real A, then a has SpectrumRestricts to realToNNReal.

Русский

Если a неотрицательно в частности 0 ≤ a и выполняются условия NonnegSpectrumClass Real A, то a имеет SpectrumRestricts к realToNNReal.

LaTeX

$$$ SpectrumRestricts\ a\ ContinuousMap.realToNNReal $$$

Lean4

theorem nnreal_of_nonneg [PartialOrder A] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) :
    SpectrumRestricts a ContinuousMap.realToNNReal :=
  nnreal_iff.mpr <| spectrum_nonneg_of_nonneg ha

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