Theorem ContinuousMap.range_toUniformOnFunIsCompact

Modification history

2024-08-29 08:05
Mathlib/Topology/UniformSpace/CompactConvergence.lean
feat: the space of continuous maps is complete if the target is complete (#16224)
Added ContinuousMap.range_toUniformOnFunIsCompactView on Github →