Def ContinuousMap.compactConvergenceFilterBasis

Modification history

2024-02-25 01:09

Mathlib/Topology/UniformSpace/CompactConvergence.lean

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

Deleted ContinuousMap.compactConvergenceFilterBasis View on Github →

2023-02-14 18:21

Mathlib/Topology/UniformSpace/CompactConvergence.lean

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

Added ContinuousMap.compactConvergenceFilterBasis View on Github →