Def ContinuousMap.toUniformOnFunIsCompact

Modification history

2024-02-25 01:09

Mathlib/Topology/UniformSpace/CompactConvergence.lean

refactor(UniformConvergenceTopology): redefine using `UniformOnFun` (#10873)

Added ContinuousMap.toUniformOnFunIsCompact View on Github →