Commit 2026-07-08 10:17 5d071905

View on Github →

feat(Topology/UniformSpace): tag UniformContinuous with @[fun_prop] (#41019) and tag all the relevant lemmas (found via Loogle). Do the same for the other function properties. The precise list of tagged function properties is UniformContinuous, UniformContinuousOn, IsUniformInducing, IsUniformEmbedding, UniformContinuous₂. From MeanFourier

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/Normed/Group/AddTorsor.lean

Modified Mathlib/Analysis/Normed/Group/Uniform.lean

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

Modified Mathlib/Analysis/Normed/Lp/ProdLp.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

Modified Mathlib/Topology/Algebra/SeparationQuotient/Section.lean

Modified Mathlib/Topology/Algebra/UniformMulAction.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

Modified Mathlib/Topology/UniformSpace/AbstractCompletion.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

modified theorem uniformContinuous_inl

modified theorem uniformContinuous_inr

Modified Mathlib/Topology/UniformSpace/Completion.lean

Modified Mathlib/Topology/UniformSpace/Defs.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean