Commit 2025-02-11 11:19 40e4ca7c

View on Github →

chore(Topology/(E)MetricSpace): move import of Topology.Bases downstream (#21657) For both EMetricSpace and PseudoMetricSpace, we have lemmas on SeparableSpace in Defs.lean that can move to Basic.lean without affecting downstream imports, but saving us an unnecessary import in Defs.lean.

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Basic.lean

added theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset

added theorem TopologicalSpace.IsSeparable.separableSpace

Modified Mathlib/Topology/EMetricSpace/Defs.lean

deleted theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset

deleted theorem TopologicalSpace.IsSeparable.separableSpace

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

added theorem ContinuousOn.isSeparable_image

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

deleted theorem ContinuousOn.isSeparable_image