Commit 2025-05-28 16:58 4bb128f3

View on Github →

feat: convenience theorems for uniform convergence (#24860)

Estimated changes

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

added theorem ContinuousMap.continuous_iff_continuous_uniformFun

added theorem ContinuousMap.continuous_iff_continuous_uniformOnFun

added theorem ContinuousMap.isUniformEmbedding_uniformFunOfFun

added theorem ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun

added theorem ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean

added theorem Filter.HasBasis.tendstoUniformlyOnFilter_iff

added theorem Filter.HasBasis.tendstoUniformlyOnFilter_iff_of_uniformity

added theorem Filter.HasBasis.tendstoUniformlyOn_iff

added theorem Filter.HasBasis.tendstoUniformlyOn_iff_of_uniformity

added theorem Filter.HasBasis.tendstoUniformly_iff

added theorem Filter.HasBasis.tendstoUniformly_iff_of_uniformity