Commit 2024-08-31 21:14 8f501100

View on Github →

feat: relate ∀ x ∈ spectrum ℝ≥0 a, x ≤ r to the ℝ-spectrum (#16340)

Estimated changes

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

added theorem QuasispectrumRestricts.le_nnreal_iff

added theorem QuasispectrumRestricts.lt_nnreal_iff

added theorem SpectrumRestricts.le_nnreal_iff

added theorem SpectrumRestricts.lt_nnreal_iff

added theorem SpectrumRestricts.nnreal_le_iff

added theorem SpectrumRestricts.nnreal_lt_iff