2022-01-05 23:45
src/topology/uniform_space/compact_convergence.lean
feat(topology/uniform_space/compact_convergence): when the domain is compact, compact convergence is just uniform convergence (#11262)
Added continuous_map.has_basis_compact_convergence_uniformity_of_compact