Theorem ContinuousMap.completeSpace_of_restrictGenTopology

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.completeSpace_of_restrictGenTopology View on Github →