Commit 2025-06-08 14:36 80b79be6

View on Github →

feat(Topology/Algebra/InfiniteSum/UniformOn): add congr lemmas (#25446) Add some congr lemmas and a locally finset range lemma.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/MultipliableUniformlyOn.lean

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

added theorem HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange

added theorem HasProdUniformlyOn.congr

added theorem HasProdUniformlyOn.congr_right

added theorem HasProdUniformlyOn.tendstoUniformlyOn_finsetRange

deleted theorem HasProdUniformlyOn.tendstoUniformlyOn_finset_range