Theorem ContinuousMap.compactConvNhd_nhd_basis

Modification history

2024-02-25 01:09

Mathlib/Topology/UniformSpace/CompactConvergence.lean

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

Deleted ContinuousMap.compactConvNhd_nhd_basis View on Github →

2023-02-14 18:21

Mathlib/Topology/UniformSpace/CompactConvergence.lean

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

Added ContinuousMap.compactConvNhd_nhd_basis View on Github →