chore(Topology): namespace lemmas around IsInducing, IsQuotientMap etc (leanprover-community#40891)

The predicates `IsInducing`, `IsEmbedding`, `IsQuotientMap` etc. were moved to the `Topology` namespace in leanprover-community#15993, but some lemmas were not moved with them, or were added outside of the namespace later. This PR moves these lemmas to the correct namespace to enable dot notation.

We do not add deprecation aliases since the lemmas only get namespaced, not renamed, and having both the lemmas and their deprecated aliases available inside the namespace could lead to trouble.

Author: peabrainiac

Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

@@ -314,8 +314,8 @@ end SpecializingMap
 section GeneralizingMap
 
 instance : (topologically GeneralizingMap).RespectsIso :=
-  topologically_respectsIso _ (fun f ↦ f.isOpenEmbedding.generalizingMap
-    f.isOpenEmbedding.isOpen_range.stableUnderGeneralization) (fun _ _ hf hg ↦ hf.comp hg)
+  topologically_respectsIso _ (fun f ↦ f.isOpenEmbedding.generalizingMap)
+    (fun _ _ hf hg ↦ hf.comp hg)
 
 instance : IsZariskiLocalAtSource (topologically GeneralizingMap) :=
   topologically_isZariskiLocalAtSource' (fun _ ↦ _) fun _ _ _ hU _ ↦ hU.generalizingMap_iff_comp

Mathlib/Condensed/TopComparison.lean

@@ -117,7 +117,7 @@ def TopCat.toSheafCompHausLike :
     apply +allowSynthFailures equalizerCondition_yonedaPresheaf
       (CompHausLike.compHausLikeToTop.{u} P) X
     intro Z B π he
-    apply IsQuotientMap.of_surjective_continuous (hs _ he) π.hom.hom.continuous
+    exact .of_surjective_continuous (hs _ he) π.hom.hom.continuous
 
 /--
 `TopCat.toSheafCompHausLike` yields a functor from `TopCat.{max u w}` to

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -500,7 +500,8 @@ is ae-measurable. -/
 theorem Continuous.aemeasurable {f : α → γ} (h : Continuous f) {μ : Measure α} : AEMeasurable f μ :=
   h.measurable.aemeasurable
 
-theorem IsClosedEmbedding.measurable {f : α → γ} (hf : IsClosedEmbedding f) : Measurable f :=
+theorem Topology.IsClosedEmbedding.measurable {f : α → γ} (hf : IsClosedEmbedding f) :
+    Measurable f :=
   hf.continuous.measurable
 
 /-- If a function is defined piecewise in terms of functions which are continuous on their

Mathlib/Topology/Constructions/SumProd.lean

@@ -800,7 +800,7 @@ theorem IsOpenMap.sumElim {f : X → Z} {g : Y → Z} (hf : IsOpenMap f) (hg : I
     IsOpenMap (Sum.elim f g) :=
   isOpenMap_sumElim.2 ⟨hf, hg⟩
 
-lemma IsOpenEmbedding.sumElim {f : X → Z} {g : Y → Z}
+lemma Topology.IsOpenEmbedding.sumElim {f : X → Z} {g : Y → Z}
     (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g) (h : Injective (Sum.elim f g)) :
     IsOpenEmbedding (Sum.elim f g) := by
   rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢
@@ -830,7 +830,7 @@ theorem IsClosedMap.sumElim {f : X → Z} {g : Y → Z} (hf : IsClosedMap f) (hg
     IsClosedMap (Sum.elim f g) :=
   isClosedMap_sumElim.2 ⟨hf, hg⟩
 
-lemma IsClosedEmbedding.sumElim {f : X → Z} {g : Y → Z}
+lemma Topology.IsClosedEmbedding.sumElim {f : X → Z} {g : Y → Z}
     (hf : IsClosedEmbedding f) (hg : IsClosedEmbedding g) (h : Injective (Sum.elim f g)) :
     IsClosedEmbedding (Sum.elim f g) := by
   rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢
@@ -974,16 +974,17 @@ theorem Topology.IsInducing.disjoint_of_sumElim_aux (h : IsInducing (Sum.elim f
     exact disjoint_image_inl_image_inr
   exact B.mono_left A
 
-theorem IsOpenEmbedding.sumSwap : IsOpenEmbedding (@Sum.swap X Y) :=
+theorem Topology.IsOpenEmbedding.sumSwap : IsOpenEmbedding (@Sum.swap X Y) :=
   (Homeomorph.sumComm X Y).isOpenEmbedding
 
-theorem IsInducing.sumSwap : IsInducing (@Sum.swap X Y) := IsOpenEmbedding.sumSwap.isInducing
+theorem Topology.IsInducing.sumSwap : IsInducing (@Sum.swap X Y) :=
+  IsOpenEmbedding.sumSwap.isInducing
 
 theorem isInducing_sumElim :
     IsInducing (Sum.elim f g) ↔ IsInducing f ∧ IsInducing g ∧
       Disjoint (closure (range f)) (range g) ∧ Disjoint (range f) (closure (range g)) :=
   ⟨fun h ↦ ⟨h.sumElim_left, h.sumElim_right, h.disjoint_of_sumElim_aux,
-    ((Sum.elim_swap ▸ h.comp IsInducing.sumSwap).disjoint_of_sumElim_aux ).symm⟩,
+    ((Sum.elim_swap ▸ h.comp .sumSwap).disjoint_of_sumElim_aux ).symm⟩,
     fun ⟨hf, hg, hFg, hfG⟩ ↦ hf.sumElim hg hFg hfG⟩
 
 lemma Topology.IsInducing.sumElim_of_separatedNhds

Mathlib/Topology/DiscreteSubset.lean

@@ -112,7 +112,7 @@ lemma IsOpenMap.isDiscrete_range [DiscreteTopology X] (hf : IsOpenMap f) :
 lemma IsDiscrete.image (hs : IsDiscrete s) (hf : IsInducing f) : IsDiscrete (f '' s) := by
   simp_all [isDiscrete_iff_nhdsWithin, ← hf.map_nhdsWithin_eq s]
 
-lemma IsInducing.isDiscrete_range [DiscreteTopology X] (hf : IsInducing f) :
+lemma Topology.IsInducing.isDiscrete_range [DiscreteTopology X] (hf : IsInducing f) :
     IsDiscrete (Set.range f) := by
   simpa using IsDiscrete.univ.image hf
 

Mathlib/Topology/Inseparable.lean

@@ -413,7 +413,7 @@ lemma Topology.IsInducing.generalizingMap (hf : IsInducing f)
   obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩
   exact ⟨_, hf.specializes_iff.mp e, rfl⟩
 
-lemma IsOpenEmbedding.generalizingMap (hf : IsOpenEmbedding f) : GeneralizingMap f :=
+lemma Topology.IsOpenEmbedding.generalizingMap (hf : IsOpenEmbedding f) : GeneralizingMap f :=
   hf.isInducing.generalizingMap hf.isOpen_range.stableUnderGeneralization
 
 lemma SpecializingMap.stableUnderSpecialization_range (h : SpecializingMap f) :

Mathlib/Topology/KrullDimension.lean

@@ -45,24 +45,24 @@ variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 ### Main dimension theorems -/
 
 /-- If `f : Y → X` is inducing, then `dim(Y) ≤ dim(X)`. -/
-theorem IsInducing.topologicalKrullDim_le {f : Y → X} (hf : IsInducing f) :
+theorem Topology.IsInducing.topologicalKrullDim_le {f : Y → X} (hf : IsInducing f) :
     topologicalKrullDim Y ≤ topologicalKrullDim X :=
   krullDim_le_of_strictMono _ (map_strictMono_of_isInducing hf)
 
 /-- The topological Krull dimension is invariant under homeomorphisms -/
 theorem IsHomeomorph.topologicalKrullDim_eq (f : X → Y) (h : IsHomeomorph f) :
     topologicalKrullDim X = topologicalKrullDim Y :=
   have fwd : topologicalKrullDim X ≤ topologicalKrullDim Y :=
-    IsInducing.topologicalKrullDim_le h.isClosedEmbedding.toIsInducing
+    h.isInducing.topologicalKrullDim_le
   have bwd : topologicalKrullDim Y ≤ topologicalKrullDim X :=
-    IsInducing.topologicalKrullDim_le (h.homeomorph f).symm.isClosedEmbedding.toIsInducing
+    (h.homeomorph f).symm.isInducing.topologicalKrullDim_le
   le_antisymm fwd bwd
 
 /-- The topological Krull dimension of any subspace is at most the dimension of the
 ambient space. -/
 theorem topologicalKrullDim_subspace_le (X : Type*) [TopologicalSpace X] (Y : Set X) :
     topologicalKrullDim Y ≤ topologicalKrullDim X :=
-  IsInducing.topologicalKrullDim_le IsInducing.subtypeVal
+  IsInducing.subtypeVal.topologicalKrullDim_le
 
 theorem topologicalKrullDim_zero_of_discreteTopology
     (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :

Mathlib/Topology/LocalAtTarget.lean

@@ -224,10 +224,7 @@ lemma isOpenMap_iff_comp : IsOpenMap f ↔ ∀ i, IsOpenMap (f ∘ ((↑) : U i
 
 lemma generalizingMap_iff_comp :
     GeneralizingMap f ↔ ∀ i, GeneralizingMap (f ∘ ((↑) : U i → α)) := by
-  refine ⟨fun hf ↦ fun i ↦
-      ((U i).isOpenEmbedding'.generalizingMap
-        (U i).isOpenEmbedding'.isOpen_range.stableUnderGeneralization).comp hf,
-    fun hf ↦ fun x y h ↦ ?_⟩
+  refine ⟨fun hf i ↦ ((U i).isOpenEmbedding'.generalizingMap).comp hf, fun hf ↦ fun x y h ↦ ?_⟩
   obtain ⟨i, hi⟩ := hU.exists_mem x
   replace h : y ⤳ (f ∘ ((↑) : U i → α)) ⟨x, hi⟩ := h
   obtain ⟨a, ha, rfl⟩ := hf i h

Mathlib/Topology/Separation/Hausdorff.lean

@@ -675,7 +675,7 @@ theorem Continuous.isClosedEmbedding [CompactSpace X] [T2Space Y] {f : X → Y}
   .of_continuous_injective_isClosedMap h hf h.isClosedMap
 
 /-- A continuous surjective map from a compact space to a Hausdorff space is a quotient map. -/
-theorem IsQuotientMap.of_surjective_continuous [CompactSpace X] [T2Space Y] {f : X → Y}
+theorem Topology.IsQuotientMap.of_surjective_continuous [CompactSpace X] [T2Space Y] {f : X → Y}
     (hsurj : Surjective f) (hcont : Continuous f) : IsQuotientMap f :=
   hcont.isClosedMap.isQuotientMap hcont hsurj