Theorem ContinuousMap.compactConvNhd_subset_compactOpen

Modification history

2024-02-25 01:09

Mathlib/Topology/UniformSpace/CompactConvergence.lean

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

Deleted ContinuousMap.compactConvNhd_subset_compactOpen View on Github →

2023-02-14 18:21

Mathlib/Topology/UniformSpace/CompactConvergence.lean

feat: port Topology.UniformSpace.CompactConvergence (#2281)

Added ContinuousMap.compactConvNhd_subset_compactOpen View on Github →