Commit 2024-04-18 14:41 742d658e

View on Github →

feat: add monotonicity theorems pertaining to the continuous functional calculus (#12224)

Estimated changes

modified theorem spectrum_nonneg_of_nonneg
added theorem algebraMap_le_cfc
added theorem cfcHom_le_iff
added theorem cfcHom_mono
added theorem cfcHom_nonneg_iff
added theorem cfc_cases
added theorem cfc_le_algebraMap
added theorem cfc_le_iff
added theorem cfc_le_one
added theorem cfc_mono
added theorem cfc_nonneg
added theorem cfc_nonneg_iff
added theorem cfc_nonpos
added theorem cfc_nonpos_iff
added theorem one_le_cfc
added theorem cfcₙHom_le_iff
added theorem cfcₙHom_mono
added theorem cfcₙHom_nonneg_iff
added theorem cfcₙ_cases
added theorem cfcₙ_le_iff
added theorem cfcₙ_mono
added theorem cfcₙ_nonneg
added theorem cfcₙ_nonneg_iff
added theorem cfcₙ_nonpos
added theorem cfcₙ_nonpos_iff