chore(Topology): generalize Topology.IsEmbedding.perfectlyNormalSpace (leanprover-community#39576)

Generalize theorem `Topology.IsEmbedding.perfectlyNormalSpace` to inducing maps. Generalize some other theorem along the way. Rename `isGδ_induced` to `IsGδ.preimage`, to match `IsOpen.preimage` and `IsClosed.preimage`.

Author: plp127

Mathlib/Topology/Baire/LocallyCompactRegular.lean

@@ -59,14 +59,15 @@ instance (priority := 100) BaireSpace.of_t2Space_locallyCompactSpace : BaireSpac
   exact hK_nonempty.mono hK_subset
 
 /-- A Gδ subset of a locally compact R₁ space is Baire. -/
-theorem IsGδ.of_t2Space_locallyCompactSpace (hG : IsGδ s) : BaireSpace s := by
-  have : BaireSpace (closure s) := by
-    convert! BaireSpace.of_t2Space_locallyCompactSpace using 1
-    · infer_instance
-    · exact isClosed_closure.locallyCompactSpace
+theorem IsGδ.baireSpace_of_t2Space_locallyCompactSpace (hG : IsGδ s) : BaireSpace s := by
+  have : LocallyCompactSpace (closure s) := isClosed_closure.locallyCompactSpace
+  have : BaireSpace (closure s) := .of_t2Space_locallyCompactSpace
   have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) :=
-    (isGδ_induced continuous_subtype_val hG).baireSpace_of_dense
+    (hG.preimage continuous_subtype_val).baireSpace_of_dense
     (by simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure])
   have h_homeo : Homeomorph ((↑) ⁻¹' s : Set (closure s)) s := ⟨⟨fun x => ⟨x, x.2⟩,
     fun x => ⟨⟨x, subset_closure x.2⟩, x.2⟩, by grind, by grind⟩, by fun_prop, by fun_prop⟩
   exact h_homeo.baireSpace
+
+@[deprecated (since := "2026-06-04")]
+alias IsGδ.of_t2Space_locallyCompactSpace := IsGδ.baireSpace_of_t2Space_locallyCompactSpace

Mathlib/Topology/GDelta/Basic.lean

@@ -152,12 +152,14 @@ theorem IsGδ.iUnion [Finite ι'] {f : ι' → Set X} (h : ∀ i, IsGδ (f i)) :
   .sUnion (finite_range _) <| forall_mem_range.2 h
 
 /-- The preimage of a Gδ set under a continuous map is Gδ. -/
-theorem isGδ_induced [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hf : Continuous f)
+theorem IsGδ.preimage [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hf : Continuous f)
     (hs : IsGδ s) : IsGδ (f ⁻¹' s) := by
   obtain ⟨U, hU1, hU2⟩ := hs.eq_iInter_nat
   simp_all only [preimage_iInter]
   exact IsGδ.iInter_of_isOpen (fun i => hf.isOpen_preimage (U i) (hU1 i))
 
+@[deprecated (since := "2026-05-19")] alias isGδ_induced := IsGδ.preimage
+
 end IsGδ
 
 section residual

Mathlib/Topology/Separation/GDelta.lean

@@ -31,7 +31,7 @@ open Function Set Filter Topology TopologicalSpace
 
 universe u
 
-variable {X : Type*} [TopologicalSpace X]
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
 section Separation
 
@@ -121,13 +121,30 @@ instance (priority := 100) [PerfectlyNormalSpace X] : R0Space X where
     intros
     solve_by_elim [hxy.mem_open]
 
+theorem Topology.IsInducing.perfectlyNormalSpace [PerfectlyNormalSpace Y] {e : X → Y}
+    (he : IsInducing e) : PerfectlyNormalSpace X where
+  toNormalSpace := he.completelyNormalSpace.toNormalSpace
+  closed_gdelta _ hs := (he.isClosed_iff.1 hs).elim fun _ ht =>
+    ht.2 ▸ ht.1.isGδ.preimage he.continuous
+
+instance {s : Set X} [PerfectlyNormalSpace X] : PerfectlyNormalSpace s :=
+  IsEmbedding.subtypeVal.perfectlyNormalSpace
+
 /-- A T₆ space is a perfectly normal T₀ space. -/
 class T6Space (X : Type u) [TopologicalSpace X] : Prop extends T0Space X, PerfectlyNormalSpace X
 
 -- see Note [lower instance priority]
 /-- A `T₆` space is a `T₅` space. -/
 instance (priority := 100) T6Space.toT5Space [T6Space X] : T5Space X where
 
+theorem Topology.IsEmbedding.t6Space [T6Space Y] {e : X → Y}
+    (he : IsEmbedding e) : T6Space X where
+  toPerfectlyNormalSpace := he.perfectlyNormalSpace
+  toT0Space := he.t0Space
+
+instance {s : Set X} [T6Space X] : T6Space s :=
+  IsEmbedding.subtypeVal.t6Space
+
 end PerfectlyNormal
 
 end Separation

Mathlib/Topology/Separation/PerfectlyNormal.lean

@@ -106,15 +106,5 @@ theorem perfectlyNormalSpace_iff_forall_isClosed_preimage_zero :
             · rcases (mem_iInter.1 h 0).1 with ⟨x, rfl⟩
               exact (hfr x).1 }
 
-theorem Topology.IsEmbedding.perfectlyNormalSpace {e : X → Y} (he : IsEmbedding e)
-    [PerfectlyNormalSpace Y] : PerfectlyNormalSpace X := by
-  rw [perfectlyNormalSpace_iff_forall_isClosed_preimage_zero]
-  intro t ht
-  obtain ⟨c, hc⟩ : ∃ c, IsClosed c ∧ e '' t = c ∩ range e := he.image_eq_isClosed_inter_range ht
-  obtain ⟨f, rfl, hf⟩ :=
-    perfectlyNormalSpace_iff_forall_isClosed_preimage_zero.1 inferInstance c hc.1
-  refine ⟨⟨f ∘ e, f.continuous.comp he.continuous⟩, ?_, fun x => hf (e x)⟩
-  simpa [Set.ext_iff, he.injective.preimage_image] using congr(e ⁻¹' $(hc.2))
-
-instance {s : Set X} [PerfectlyNormalSpace X] : PerfectlyNormalSpace s :=
-  IsEmbedding.subtypeVal.perfectlyNormalSpace
+@[deprecated (since := "2026-06-03")]
+alias Topology.IsEmbedding.perfectlyNormalSpace := Topology.IsInducing.perfectlyNormalSpace

Mathlib/Topology/Separation/Regular.lean

@@ -595,10 +595,10 @@ instance (priority := 100) CompletelyNormalSpace.toNormalSpace
   normal s t hs ht hd := separatedNhds_iff_disjoint.2 <|
     completely_normal (by rwa [hs.closure_eq]) (by rwa [ht.closure_eq])
 
-theorem Topology.IsEmbedding.completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSpace Y]
-    {e : X → Y} (he : IsEmbedding e) : CompletelyNormalSpace X := by
+theorem Topology.IsInducing.completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSpace Y]
+    {e : X → Y} (he : IsInducing e) : CompletelyNormalSpace X := by
   refine ⟨fun s t hd₁ hd₂ => ?_⟩
-  simp only [he.isInducing.nhdsSet_eq_comap]
+  simp only [he.nhdsSet_eq_comap]
   refine disjoint_comap (completely_normal ?_ ?_)
   · rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
       ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
@@ -665,10 +665,8 @@ class T5Space (X : Type u) [TopologicalSpace X] : Prop extends T1Space X, Comple
 
 theorem Topology.IsEmbedding.t5Space [TopologicalSpace Y] [T5Space Y] {e : X → Y}
     (he : IsEmbedding e) : T5Space X where
-  __ := he.t1Space
-  completely_normal := by
-    have := he.completelyNormalSpace
-    exact completely_normal
+  toCompletelyNormalSpace := he.completelyNormalSpace
+  toT1Space := he.t1Space
 
 protected theorem Homeomorph.t5Space [TopologicalSpace Y] [T5Space X] (h : X ≃ₜ Y) : T5Space Y :=
   h.symm.isClosedEmbedding.t5Space