chore: move TopologicalSpace.SecondCountableTopology into the root namespace (#8186)

sgouezel · sgouezel · commit 4a70d87f9991 · 2023-11-08T06:59:37.000Z
All the other properties of topological spaces like T0Space or RegularSpace are in the root namespace. Many files were opening `TopologicalSpace` just for the sake of shortening `TopologicalSpace.SecondCountableTopology`...
diff --git a/Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean
@@ -20,7 +20,6 @@ directed by `v`.
 -/
 
 open MeasureTheory
-open TopologicalSpace (SecondCountableTopology)
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [OpensMeasurableSpace E]
diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
@@ -51,7 +51,7 @@ theorem continuous_im : Continuous im :=
   Complex.continuous_im.comp continuous_coe
 #align upper_half_plane.continuous_im UpperHalfPlane.continuous_im
 
-instance : TopologicalSpace.SecondCountableTopology ℍ :=
+instance : SecondCountableTopology ℍ :=
   TopologicalSpace.Subtype.secondCountableTopology _
 
 instance : T3Space ℍ := Subtype.t3Space
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
@@ -597,7 +597,7 @@ instance instLocallyConvexSpace : LocallyConvexSpace ℝ 𝓢(E, F) :=
   (schwartz_withSeminorms ℝ E F).toLocallyConvexSpace
 #align schwartz_map.locally_convex_space SchwartzMap.instLocallyConvexSpace
 
-instance instFirstCountableTopology : TopologicalSpace.FirstCountableTopology 𝓢(E, F) :=
+instance instFirstCountableTopology : FirstCountableTopology 𝓢(E, F) :=
   (schwartz_withSeminorms ℝ E F).first_countable
 #align schwartz_map.topological_space.first_countable_topology SchwartzMap.instFirstCountableTopology
 
diff --git a/Mathlib/Analysis/Fourier/FourierTransform.lean b/Mathlib/Analysis/Fourier/FourierTransform.lean
@@ -161,7 +161,7 @@ theorem fourierIntegral_add (he : Continuous e) (hL : Continuous fun p : V × W
 #align vector_fourier.fourier_integral_add VectorFourier.fourierIntegral_add
 
 /-- The Fourier integral of an `L^1` function is a continuous function. -/
-theorem fourierIntegral_continuous [TopologicalSpace.FirstCountableTopology W] (he : Continuous e)
+theorem fourierIntegral_continuous [FirstCountableTopology W] (he : Continuous e)
     (hL : Continuous fun p : V × W => L p.1 p.2) {f : V → E} (hf : Integrable f μ) :
     Continuous (fourierIntegral e μ L f) := by
   apply continuous_of_dominated
diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
@@ -968,7 +968,7 @@ variable [TopologicalSpace E]
 /-- If the topology of a space is induced by a countable family of seminorms, then the topology
 is first countable. -/
 theorem WithSeminorms.first_countable (hp : WithSeminorms p) :
-    TopologicalSpace.FirstCountableTopology E := by
+    FirstCountableTopology E := by
   have := hp.topologicalAddGroup
   let _ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
   have : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
diff --git a/Mathlib/MeasureTheory/Function/SpecialFunctions/Inner.lean b/Mathlib/MeasureTheory/Function/SpecialFunctions/Inner.lean
@@ -21,26 +21,26 @@ local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
 
 @[aesop safe 20 apply (rule_sets [Measurable])]
 theorem Measurable.inner {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
-    [TopologicalSpace.SecondCountableTopology E] {f g : α → E} (hf : Measurable f)
+    [SecondCountableTopology E] {f g : α → E} (hf : Measurable f)
     (hg : Measurable g) : Measurable fun t => ⟪f t, g t⟫ :=
   Continuous.measurable2 continuous_inner hf hg
 #align measurable.inner Measurable.inner
 
 @[measurability]
 theorem Measurable.const_inner {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
-    [TopologicalSpace.SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
+    [SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
     Measurable fun t => ⟪c, f t⟫ :=
   Measurable.inner measurable_const hf
 
 @[measurability]
 theorem Measurable.inner_const {_ : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
-    [TopologicalSpace.SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
+    [SecondCountableTopology E] {c : E} {f : α → E} (hf : Measurable f) :
     Measurable fun t => ⟪f t, c⟫ :=
   Measurable.inner hf measurable_const
 
 @[aesop safe 20 apply (rule_sets [Measurable])]
 theorem AEMeasurable.inner {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
-    [TopologicalSpace.SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f g : α → E}
+    [SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f g : α → E}
     (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun x => ⟪f x, g x⟫) μ := by
   refine' ⟨fun x => ⟪hf.mk f x, hg.mk g x⟫, hf.measurable_mk.inner hg.measurable_mk, _⟩
   refine' hf.ae_eq_mk.mp (hg.ae_eq_mk.mono fun x hxg hxf => _)
@@ -51,15 +51,15 @@ theorem AEMeasurable.inner {m : MeasurableSpace α} [MeasurableSpace E] [OpensMe
 set_option linter.unusedVariables false in
 @[measurability]
 theorem AEMeasurable.const_inner {m : MeasurableSpace α} [MeasurableSpace E]
-    [OpensMeasurableSpace E] [TopologicalSpace.SecondCountableTopology E]
+    [OpensMeasurableSpace E] [SecondCountableTopology E]
     {μ : MeasureTheory.Measure α} {f : α → E} {c : E} (hf : AEMeasurable f μ) :
     AEMeasurable (fun x => ⟪c, f x⟫) μ :=
   AEMeasurable.inner aemeasurable_const hf
 
 set_option linter.unusedVariables false in
 @[measurability]
 theorem AEMeasurable.inner_const {m : MeasurableSpace α} [MeasurableSpace E]
-    [OpensMeasurableSpace E] [TopologicalSpace.SecondCountableTopology E]
+    [OpensMeasurableSpace E] [SecondCountableTopology E]
     {μ : MeasureTheory.Measure α} {f : α → E} {c : E} (hf : AEMeasurable f μ) :
     AEMeasurable (fun x => ⟪f x, c⟫) μ :=
   AEMeasurable.inner hf aemeasurable_const
diff --git a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
@@ -71,7 +71,7 @@ section BochnerIntegral
 
 variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X]
 variable (μ : Measure X)
-variable {E : Type*} [NormedAddCommGroup E] [TopologicalSpace.SecondCountableTopology E]
+variable {E : Type*} [NormedAddCommGroup E] [SecondCountableTopology E]
 variable [MeasurableSpace E] [BorelSpace E]
 
 lemma lintegral_nnnorm_le (f : X →ᵇ E) :
diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
@@ -145,8 +145,6 @@ set_option autoImplicit true
 
 noncomputable section
 
-open TopologicalSpace (SecondCountableTopology)
-
 open MeasureTheory Set Classical Filter Function
 
 open scoped Classical Topology Filter ENNReal BigOperators Interval NNReal
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
@@ -50,8 +50,6 @@ integral
 
 noncomputable section
 
-open TopologicalSpace (SecondCountableTopology)
-
 open MeasureTheory Set Classical Filter Function
 
 open scoped Classical Topology Filter ENNReal BigOperators Interval NNReal
diff --git a/Mathlib/MeasureTheory/Integral/LebesgueNormedSpace.lean b/Mathlib/MeasureTheory/Integral/LebesgueNormedSpace.lean
@@ -18,7 +18,7 @@ open NNReal ENNReal
 variable {α β γ δ : Type*} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
 
 theorem aemeasurable_withDensity_iff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-    [TopologicalSpace.SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {f : α → ℝ≥0}
+    [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {f : α → ℝ≥0}
     (hf : Measurable f) {g : α → E} :
     AEMeasurable g (μ.withDensity fun x => (f x : ℝ≥0∞)) ↔
       AEMeasurable (fun x => (f x : ℝ) • g x) μ := by
diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean
@@ -1042,14 +1042,14 @@ theorem hausdorffMeasure_pi_real {ι : Type*} [Fintype ι] :
 variable (ι X)
 
 theorem hausdorffMeasure_measurePreserving_funUnique [Unique ι]
-    [TopologicalSpace.SecondCountableTopology X] (d : ℝ) :
+    [SecondCountableTopology X] (d : ℝ) :
     MeasurePreserving (MeasurableEquiv.funUnique ι X) μH[d] μH[d] :=
   (IsometryEquiv.funUnique ι X).measurePreserving_hausdorffMeasure _
 #align measure_theory.hausdorff_measure_measure_preserving_fun_unique MeasureTheory.hausdorffMeasure_measurePreserving_funUnique
 
 theorem hausdorffMeasure_measurePreserving_piFinTwo (α : Fin 2 → Type*)
     [∀ i, MeasurableSpace (α i)] [∀ i, EMetricSpace (α i)] [∀ i, BorelSpace (α i)]
-    [∀ i, TopologicalSpace.SecondCountableTopology (α i)] (d : ℝ) :
+    [∀ i, SecondCountableTopology (α i)] (d : ℝ) :
     MeasurePreserving (MeasurableEquiv.piFinTwo α) μH[d] μH[d] :=
   (IsometryEquiv.piFinTwo α).measurePreserving_hausdorffMeasure _
 #align measure_theory.hausdorff_measure_measure_preserving_pi_fin_two MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -96,9 +96,6 @@ open Set
 open Filter hiding map
 
 open Function MeasurableSpace
-
-open TopologicalSpace (SecondCountableTopology)
-
 open Classical Topology BigOperators Filter ENNReal NNReal Interval MeasureTheory
 
 variable {α β γ δ ι R R' : Type*}
@@ -543,7 +540,7 @@ theorem tendsto_measure_iInter [Countable ι] [Preorder ι] [IsDirected ι (· 
 /-- The measure of the intersection of a decreasing sequence of measurable
 sets indexed by a linear order with first countable topology is the limit of the measures. -/
 theorem tendsto_measure_biInter_gt {ι : Type*} [LinearOrder ι] [TopologicalSpace ι]
-    [OrderTopology ι] [DenselyOrdered ι] [TopologicalSpace.FirstCountableTopology ι] {s : ι → Set α}
+    [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] {s : ι → Set α}
     {a : ι} (hs : ∀ r > a, MeasurableSet (s r)) (hm : ∀ i j, a < i → i ≤ j → s i ⊆ s j)
     (hf : ∃ r > a, μ (s r) ≠ ∞) : Tendsto (μ ∘ s) (𝓝[Ioi a] a) (𝓝 (μ (⋂ r > a, s r))) := by
   refine' tendsto_order.2 ⟨fun l hl => _, fun L hL => _⟩
diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
@@ -56,9 +56,6 @@ outer measure, Carathéodory-measurable, Carathéodory's criterion
 noncomputable section
 
 open Set Function Filter
-
-open TopologicalSpace (SecondCountableTopology)
-
 open Classical BigOperators NNReal Topology ENNReal MeasureTheory
 
 namespace MeasureTheory
diff --git a/Mathlib/MeasureTheory/Measure/Regular.lean b/Mathlib/MeasureTheory/Measure/Regular.lean
@@ -629,7 +629,7 @@ instance (priority := 100) of_pseudoEMetricSpace_of_isFiniteMeasure {X : Type*}
 /-- Any locally finite measure on a second countable metric space (or even a pseudo emetric space)
 is weakly regular. -/
 instance (priority := 100) of_pseudoEMetric_secondCountable_of_locallyFinite {X : Type*}
-    [PseudoEMetricSpace X] [TopologicalSpace.SecondCountableTopology X] [MeasurableSpace X]
+    [PseudoEMetricSpace X] [SecondCountableTopology X] [MeasurableSpace X]
     [BorelSpace X] (μ : Measure X) [IsLocallyFiniteMeasure μ] : WeaklyRegular μ :=
   haveI : OuterRegular μ := by
     refine' (μ.finiteSpanningSetsInOpen'.mono' fun U hU => _).outerRegular
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@@ -1265,7 +1265,7 @@ theorem Summable.tendsto_atTop_zero {f : ℕ → G} (hf : Summable f) : Tendsto
   exact hf.tendsto_cofinite_zero
 #align summable.tendsto_at_top_zero Summable.tendsto_atTop_zero
 
-theorem Summable.countable_support [TopologicalSpace.FirstCountableTopology G] [T1Space G]
+theorem Summable.countable_support [FirstCountableTopology G] [T1Space G]
     (hf : Summable f) : f.support.Countable := by
   simpa only [ker_nhds] using hf.tendsto_cofinite_zero.countable_compl_preimage_ker
 
diff --git a/Mathlib/Topology/Algebra/Order/LeftRightLim.lean b/Mathlib/Topology/Algebra/Order/LeftRightLim.lean
@@ -237,7 +237,7 @@ theorem continuousAt_iff_leftLim_eq_rightLim : ContinuousAt f x ↔ leftLim f x
 /-- In a second countable space, the set of points where a monotone function is not right-continuous
 is at most countable. Superseded by `countable_not_continuousAt` which gives the two-sided
 version. -/
-theorem countable_not_continuousWithinAt_Ioi [TopologicalSpace.SecondCountableTopology β] :
+theorem countable_not_continuousWithinAt_Ioi [SecondCountableTopology β] :
     Set.Countable { x | ¬ContinuousWithinAt f (Ioi x) x } := by
   apply (countable_image_lt_image_Ioi f).mono
   rintro x (hx : ¬ContinuousWithinAt f (Ioi x) x)
@@ -255,14 +255,14 @@ theorem countable_not_continuousWithinAt_Ioi [TopologicalSpace.SecondCountableTo
 /-- In a second countable space, the set of points where a monotone function is not left-continuous
 is at most countable. Superseded by `countable_not_continuousAt` which gives the two-sided
 version. -/
-theorem countable_not_continuousWithinAt_Iio [TopologicalSpace.SecondCountableTopology β] :
+theorem countable_not_continuousWithinAt_Iio [SecondCountableTopology β] :
     Set.Countable { x | ¬ContinuousWithinAt f (Iio x) x } :=
   hf.dual.countable_not_continuousWithinAt_Ioi
 #align monotone.countable_not_continuous_within_at_Iio Monotone.countable_not_continuousWithinAt_Iio
 
 /-- In a second countable space, the set of points where a monotone function is not continuous
 is at most countable. -/
-theorem countable_not_continuousAt [TopologicalSpace.SecondCountableTopology β] :
+theorem countable_not_continuousAt [SecondCountableTopology β] :
     Set.Countable { x | ¬ContinuousAt f x } := by
   apply
     (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).mono
@@ -355,7 +355,7 @@ theorem continuousAt_iff_leftLim_eq_rightLim : ContinuousAt f x ↔ leftLim f x
 
 /-- In a second countable space, the set of points where an antitone function is not continuous
 is at most countable. -/
-theorem countable_not_continuousAt [TopologicalSpace.SecondCountableTopology β] :
+theorem countable_not_continuousAt [SecondCountableTopology β] :
     Set.Countable { x | ¬ContinuousAt f x } :=
   hf.dual_right.countable_not_continuousAt
 #align antitone.countable_not_continuous_at Antitone.countable_not_continuousAt
diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean
@@ -26,9 +26,9 @@ conditions are equivalent in this case).
 * `TopologicalSpace.IsTopologicalBasis s`: The topological space `t` has basis `s`.
 * `TopologicalSpace.SeparableSpace α`: The topological space `t` has a countable, dense subset.
 * `TopologicalSpace.IsSeparable s`: The set `s` is contained in the closure of a countable set.
-* `TopologicalSpace.FirstCountableTopology α`: A topology in which `𝓝 x` is countably generated for
+* `FirstCountableTopology α`: A topology in which `𝓝 x` is countably generated for
   every `x`.
-* `TopologicalSpace.SecondCountableTopology α`: A topology which has a topological basis which is
+* `SecondCountableTopology α`: A topology which has a topological basis which is
   countable.
 
 ## Main results
@@ -39,16 +39,16 @@ conditions are equivalent in this case).
   the union of arbitrarily-many open sets is equal to a sub-union of only countably many of these
   sets.
 * `TopologicalSpace.SecondCountableTopology.countable_cover_nhds`: Consider `f : α → Set α` with the
-  property that `f x ∈ 𝓝 x` for all `x`. Then there is some countable set `s` whose image covers the
-  space.
+  property that `f x ∈ 𝓝 x` for all `x`. Then there is some countable set `s` whose image covers
+  the space.
 
 ## Implementation Notes
 For our applications we are interested that there exists a countable basis, but we do not need the
 concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.
 
 ### TODO:
 
-More fine grained instances for `TopologicalSpace.FirstCountableTopology`,
+More fine grained instances for `FirstCountableTopology`,
 `TopologicalSpace.SeparableSpace`, and more.
 -/
 
@@ -303,10 +303,10 @@ variable (α)
 `TopologicalSpace.denseRange_denseSeq`.
 
 If `α` is a uniform space with countably generated uniformity filter (e.g., an `EMetricSpace`), then
-this condition is equivalent to `TopologicalSpace.SecondCountableTopology α`. In this case the
+this condition is equivalent to `SecondCountableTopology α`. In this case the
 latter should be used as a typeclass argument in theorems because Lean can automatically deduce
-`TopologicalSpace.SeparableSpace` from `TopologicalSpace.SecondCountableTopology` but it can't
-deduce `TopologicalSpace.SecondCountableTopology` from `TopologicalSpace.SeparableSpace`.
+`TopologicalSpace.SeparableSpace` from `SecondCountableTopology` but it can't
+deduce `SecondCountableTopology` from `TopologicalSpace.SeparableSpace`.
 
 Porting note: TODO: the previous paragraph describes the state of the art in Lean 3. We can have
 instance cycles in Lean 4 but we might want to postpone adding them till after the port. -/
@@ -620,10 +620,10 @@ variable (α : Type u) [t : TopologicalSpace α]
 
 /-- A first-countable space is one in which every point has a
   countable neighborhood basis. -/
-class FirstCountableTopology : Prop where
+class _root_.FirstCountableTopology : Prop where
   /-- The filter `𝓝 a` is countably generated for all points `a`. -/
   nhds_generated_countable : ∀ a : α, (𝓝 a).IsCountablyGenerated
-#align topological_space.first_countable_topology TopologicalSpace.FirstCountableTopology
+#align topological_space.first_countable_topology FirstCountableTopology
 
 attribute [instance] FirstCountableTopology.nhds_generated_countable
 
@@ -662,10 +662,10 @@ instance isCountablyGenerated_nhdsWithin (x : α) [IsCountablyGenerated (𝓝 x)
 variable (α)
 
 /-- A second-countable space is one with a countable basis. -/
-class SecondCountableTopology : Prop where
+class _root_.SecondCountableTopology : Prop where
   /-- There exists a countable set of sets that generates the topology. -/
   is_open_generated_countable : ∃ b : Set (Set α), b.Countable ∧ t = TopologicalSpace.generateFrom b
-#align topological_space.second_countable_topology TopologicalSpace.SecondCountableTopology
+#align topological_space.second_countable_topology SecondCountableTopology
 
 variable {α}
 
diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
@@ -254,8 +254,8 @@ noncomputable def ofEmbedding (f : X → Y) (hf : Embedding f) : X ≃ₜ Set.ra
   toEquiv := Equiv.ofInjective f hf.inj
 #align homeomorph.of_embedding Homeomorph.ofEmbedding
 
-protected theorem secondCountableTopology [TopologicalSpace.SecondCountableTopology Y]
-    (h : X ≃ₜ Y) : TopologicalSpace.SecondCountableTopology X :=
+protected theorem secondCountableTopology [SecondCountableTopology Y]
+    (h : X ≃ₜ Y) : SecondCountableTopology X :=
   h.inducing.secondCountableTopology
 #align homeomorph.second_countable_topology Homeomorph.secondCountableTopology
 
diff --git a/Mathlib/Topology/Instances/NNReal.lean b/Mathlib/Topology/Instances/NNReal.lean
@@ -20,7 +20,7 @@ Instances for the following typeclasses are defined:
 
 * `TopologicalSpace ℝ≥0`
 * `TopologicalSemiring ℝ≥0`
-* `TopologicalSpace.SecondCountableTopology ℝ≥0`
+* `SecondCountableTopology ℝ≥0`
 * `OrderTopology ℝ≥0`
 * `ContinuousSub ℝ≥0`
 * `HasContinuousInv₀ ℝ≥0` (continuity of `x⁻¹` away from `0`)
diff --git a/Mathlib/Topology/LocalHomeomorph.lean b/Mathlib/Topology/LocalHomeomorph.lean
@@ -47,8 +47,6 @@ then it should use `e.source ∩ s` or `e.target ∩ t`, not `s ∩ e.source` or
 
 open Function Set Filter Topology
 
-open TopologicalSpace (SecondCountableTopology)
-
 variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} [TopologicalSpace α]
   [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ]
 
diff --git a/Mathlib/Topology/Metrizable/Basic.lean b/Mathlib/Topology/Metrizable/Basic.lean
@@ -58,7 +58,7 @@ theorem _root_.Inducing.pseudoMetrizableSpace [PseudoMetrizableSpace Y] {f : X 
 
 /-- Every pseudo-metrizable space is first countable. -/
 instance (priority := 100) PseudoMetrizableSpace.firstCountableTopology
-    [h : PseudoMetrizableSpace X] : TopologicalSpace.FirstCountableTopology X := by
+    [h : PseudoMetrizableSpace X] : FirstCountableTopology X := by
   rcases h with ⟨_, hm⟩
   rw [← hm]
   exact @UniformSpace.firstCountableTopology X PseudoMetricSpace.toUniformSpace
diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean
@@ -1326,7 +1326,7 @@ variable (α)
 /-- Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then
 it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see
 [double arrow space](https://topology.pi-base.org/spaces/S000093) for a counterexample. -/
-theorem TopologicalSpace.SecondCountableTopology.of_separableSpace_orderTopology [DenselyOrdered α]
+theorem SecondCountableTopology.of_separableSpace_orderTopology [DenselyOrdered α]
     [SeparableSpace α] : SecondCountableTopology α := by
   rcases exists_countable_dense α with ⟨s, hc, hd⟩
   refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
diff --git a/Mathlib/Topology/Sequences.lean b/Mathlib/Topology/Sequences.lean
