Theorem CompactExhaustion.exists_superset_of_isCompact

Modification history

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