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`.

Author: Vierkantor

Mathlib/Topology/EMetricSpace/Basic.lean

@@ -296,3 +296,35 @@ instance [PseudoEMetricSpace X] : EMetricSpace (SeparationQuotient X) :=
       toUniformSpace := inferInstance,
       uniformity_edist := comap_injective (surjective_mk.prodMap surjective_mk) <| by
         simp [comap_mk_uniformity, PseudoEMetricSpace.uniformity_edist] } _
+
+namespace TopologicalSpace
+
+section Compact
+
+open Topology
+
+/-- If a set `s` is separable in a (pseudo extended) metric space, then it admits a countable dense
+subset. This is not obvious, as the countable set whose closure covers `s` given by the definition
+of separability does not need in general to be contained in `s`. -/
+theorem IsSeparable.exists_countable_dense_subset
+    {s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t := by
+  have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 => by
+    rcases hs with ⟨t, htc, hst⟩
+    refine ⟨t, htc, hst.trans fun x hx => ?_⟩
+    rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
+    exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩
+  exact subset_countable_closure_of_almost_dense_set _ this
+
+/-- If a set `s` is separable, then the corresponding subtype is separable in a (pseudo extended)
+metric space.  This is not obvious, as the countable set whose closure covers `s` does not need in
+general to be contained in `s`. -/
+theorem IsSeparable.separableSpace {s : Set α} (hs : IsSeparable s) :
+    SeparableSpace s := by
+  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩
+  lift t to Set s using hts
+  refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩
+  rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]
+
+end Compact
+
+end TopologicalSpace

Mathlib/Topology/EMetricSpace/Defs.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
 -/
 import Mathlib.Data.ENNReal.Inv
-import Mathlib.Topology.Bases
 import Mathlib.Topology.UniformSpace.Basic
 import Mathlib.Topology.UniformSpace.OfFun
 
@@ -535,30 +534,6 @@ theorem subset_countable_closure_of_almost_dense_set (s : Set α)
     edist x (f n⁻¹ y) ≤ (n : ℝ≥0∞)⁻¹ * 2 := hf _ _ ⟨hyx, hx⟩
     _ < ε := ENNReal.mul_lt_of_lt_div hn
 
-open TopologicalSpace in
-/-- If a set `s` is separable in a (pseudo extended) metric space, then it admits a countable dense
-subset. This is not obvious, as the countable set whose closure covers `s` given by the definition
-of separability does not need in general to be contained in `s`. -/
-theorem _root_.TopologicalSpace.IsSeparable.exists_countable_dense_subset
-    {s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t := by
-  have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 => by
-    rcases hs with ⟨t, htc, hst⟩
-    refine ⟨t, htc, hst.trans fun x hx => ?_⟩
-    rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
-    exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩
-  exact subset_countable_closure_of_almost_dense_set _ this
-
-open TopologicalSpace in
-/-- If a set `s` is separable, then the corresponding subtype is separable in a (pseudo extended)
-metric space.  This is not obvious, as the countable set whose closure covers `s` does not need in
-general to be contained in `s`. -/
-theorem _root_.TopologicalSpace.IsSeparable.separableSpace {s : Set α} (hs : IsSeparable s) :
-    SeparableSpace s := by
-  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩
-  lift t to Set s using hts
-  refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩
-  rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]
-
 end Compact
 
 end EMetric

Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

@@ -270,3 +270,9 @@ theorem finite_cover_balls_of_compact {α : Type u} [PseudoMetricSpace α] {s :
 alias IsCompact.finite_cover_balls := finite_cover_balls_of_compact
 
 end Compact
+
+/-- If a map is continuous on a separable set `s`, then the image of `s` is also separable. -/
+theorem ContinuousOn.isSeparable_image [TopologicalSpace β] {f : α → β} {s : Set α}
+    (hf : ContinuousOn f s) (hs : IsSeparable s) : IsSeparable (f '' s) := by
+  rw [image_eq_range, ← image_univ]
+  exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict

Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

@@ -1141,12 +1141,6 @@ theorem dense_iff_iUnion_ball (s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s,
 theorem denseRange_iff {f : β → α} : DenseRange f ↔ ∀ x, ∀ r > 0, ∃ y, dist x (f y) < r :=
   forall_congr' fun x => by simp only [mem_closure_iff, exists_range_iff]
 
-/-- If a map is continuous on a separable set `s`, then the image of `s` is also separable. -/
-theorem _root_.ContinuousOn.isSeparable_image [TopologicalSpace β] {f : α → β} {s : Set α}
-    (hf : ContinuousOn f s) (hs : IsSeparable s) : IsSeparable (f '' s) := by
-  rw [image_eq_range, ← image_univ]
-  exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict
-
 end Metric
 
 instance : PseudoMetricSpace (Additive α) := ‹_›