Theorem CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity

Modification history

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