Theorem ContinuousMap.mem_compactConvergence_nhd_filter

Modification history

2024-02-25 01:09

Mathlib/Topology/UniformSpace/CompactConvergence.lean

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

Deleted ContinuousMap.mem_compactConvergence_nhd_filter View on Github →

2023-02-14 18:21

Mathlib/Topology/UniformSpace/CompactConvergence.lean

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

Added ContinuousMap.mem_compactConvergence_nhd_filter View on Github →