Commit 2025-05-31 21:25 6565d316

View on Github →

feat: continuity of the continuous functional calculus in each variable (#24866)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Continuity.lean

added theorem Continuous.cfc_fun

added theorem Continuous.cfc_nnreal

added theorem Continuous.cfcₙ_fun

added theorem Continuous.cfcₙ_nnreal

added theorem ContinuousAt.cfc_nnreal

added theorem ContinuousAt.cfcₙ_nnreal

added theorem ContinuousOn.cfc_fun

added theorem ContinuousOn.cfc_nnreal

added theorem ContinuousOn.cfcₙ_fun

added theorem ContinuousOn.cfcₙ_nnreal

added theorem ContinuousWithinAt.cfc_nnreal

added theorem ContinuousWithinAt.cfcₙ_nnreal

added theorem Filter.Tendsto.cfc_nnreal

added theorem Filter.Tendsto.cfcₙ_nnreal

added theorem continuousAt_cfc_fun

added theorem continuousAt_cfcₙ_fun

added theorem continuousOn_cfc

added theorem continuousOn_cfc_nnreal

added theorem continuousOn_cfcₙ

added theorem continuousOn_cfcₙ_nnreal

added theorem continuousWithinAt_cfc_fun

added theorem continuousWithinAt_cfcₙ_fun

added theorem continuous_cfcHomSuperset_left

added theorem continuous_cfcₙ

added theorem continuous_cfcₙHomSuperset_left

added theorem tendsto_cfc_fun

added theorem tendsto_cfcₙ_fun

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

added def Set.zeroOfFactMem

Modified Mathlib/Topology/Instances/NNReal/Lemmas.lean