Commit 2025-10-15 11:11 06bd3096

View on Github →

feat: missing basic API for uniformly continuous functions (#30531)

Estimated changes

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem UniformContinuous.comp_uniformContinuousOn

modified theorem UniformContinuous.continuous

added theorem UniformContinuous.uniformContinuousOn

added theorem UniformContinuousOn.comp

added theorem UniformContinuousOn.mono

added theorem uniformContinuous_swap

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean