Commit 2025-11-26 06:17 01e172ec

View on Github →

feat(HasSumUniformlyOn): generalize theorem (#31313) Drop the T2Space assumption which was never really needed in MultipliableUniformlyOn.hasProdUniformlyOn and SummableUniformlyOn.hasSumUniformlyOn.

Estimated changes

Modified Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean

modified theorem MultipliableLocallyUniformly.hasProdLocallyUniformly

modified theorem MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn

modified theorem MultipliableLocallyUniformlyOn_congr

modified theorem MultipliableUniformly.hasProdUniformly

modified theorem MultipliableUniformlyOn.hasProdUniformlyOn

modified theorem multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn

modified theorem multipliableLocallyUniformlyOn_of_of_forall_exists_nhds

modified theorem multipliableLocallyUniformly_iff_hasProdLocallyUniformly

modified theorem multipliableLocallyUniformly_of_of_forall_exists_nhds

deleted theorem multipliableUniformlyOn_iff_hasProdUniformlyOn

modified theorem multipliableUniformly_iff_hasProdUniformly

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean

added theorem TendstoLocallyUniformly.congr

added theorem TendstoLocallyUniformly.congr_inseparable

added theorem TendstoLocallyUniformly.congr_inseparable_right

added theorem TendstoLocallyUniformly.congr_right

added theorem TendstoLocallyUniformlyOn.congr_inseparable

added theorem TendstoLocallyUniformlyOn.congr_inseparable_right

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean

added theorem TendstoUniformlyOn.congr_inseparable

added theorem TendstoUniformlyOn.congr_inseparable_right

added theorem TendstoUniformlyOnFilter.congr_inseparable

added theorem tendstoUniformly_congr_inseparable