Theorem IsCompact.exists_countable_dense_subset

Modification history

2026-09-29 23:48
Mathlib/Topology/Metrizable/Basic.lean
chore(Topology/Metrizable): generalize compact separability (#43067)
Added IsCompact.exists_countable_dense_subsetView on Github →