Commit 2025-07-07 23:23 7e05fd87

View on Github →

feat: refactor and expand lemmas about integration and continuous functional calculus (#26041)

Estimated changes

modified theorem cfcHom_integral
added theorem cfcL_integrable
modified theorem cfcL_integral
modified theorem cfc_integral'
modified theorem cfc_integral
added theorem cfc_setIntegral'
added theorem cfc_setIntegral
modified theorem cfcₙHom_integral
added theorem cfcₙL_integrable
modified theorem cfcₙL_integral
modified theorem cfcₙ_integral'
modified theorem cfcₙ_integral
added theorem cfcₙ_setIntegral'
added theorem cfcₙ_setIntegral
added theorem integrableOn_cfc'
added theorem integrableOn_cfc
added theorem integrableOn_cfcₙ'
added theorem integrableOn_cfcₙ
added theorem integrable_cfc'
added theorem integrable_cfc
added theorem integrable_cfcₙ'
added theorem integrable_cfcₙ
added theorem cfcₙ_apply_mkD
added theorem cfcₙ_eq_cfcₙL
added theorem cfcₙ_eq_cfcₙL_mkD
added theorem cfc_apply_mkD
added theorem cfc_eq_cfcL_mkD