Commit 2026-09-29 23:48 60c5ebd1

View on Github →

chore(Topology/Metrizable): generalize compact separability (#43067)

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Basic.lean

deleted theorem EMetric.subset_countable_closure_of_compact

Modified Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

deleted theorem IsCompact.isSeparable

Modified Mathlib/Topology/Metrizable/Basic.lean

added theorem IsCompact.exists_countable_dense_subset

added theorem IsCompact.isSeparable