Theorem CompactExhaustion.hasBasis_compactConvergenceUniformity

Modification history

2024-03-08 18:41
Mathlib/Topology/UniformSpace/CompactConvergence.lean
feat(UniformSpace/CompactConvergence): prove metrizability (#10942)
Added CompactExhaustion.hasBasis_compactConvergenceUniformityView on Github →