Commit 2024-05-23 13:06 9f80e7c0

View on Github →

feat: functoriality of ContinuousMap in uniform spaces (#13019)

Estimated changes

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

added theorem ContinuousMap.uniformContinuous_comp

added theorem ContinuousMap.uniformContinuous_comp_left

added theorem ContinuousMap.uniformEmbedding_comp

added theorem ContinuousMap.uniformInducing_comp