[Merged by Bors] - feat: generalize Topology/OpenPartialHomeomorph/Basic to PartialHomeomorph

Mathlib.lean

@@ -8126,6 +8126,7 @@ public import Mathlib.Topology.Order.T5
 public import Mathlib.Topology.Order.UpperLowerSetTopology
 public import Mathlib.Topology.Order.WithTop
 public import Mathlib.Topology.Partial
+public import Mathlib.Topology.PartialHomeomorph.Basic
 public import Mathlib.Topology.PartialHomeomorph.Defs
 public import Mathlib.Topology.PartitionOfUnity
 public import Mathlib.Topology.Path

Mathlib/Logic/Equiv/PartialEquiv.lean

@@ -284,6 +284,14 @@ protected def toEquiv : e.source ≃ e.target where
   left_inv := fun ⟨_, hx⟩ => Subtype.ext <| e.left_inv hx
   right_inv := fun ⟨_, hy⟩ => Subtype.ext <| e.right_inv hy
 
+lemma toEquiv_eq_codRestrict_restrict :
+    e.toEquiv = codRestrict (e.source.domRestrict e) e.target (by simp) :=
+  rfl
+
+lemma toEquiv_symm_eq_codRestrict_restrict :
+    e.toEquiv.symm = codRestrict (e.target.domRestrict e.invFun) e.source (by simp) := by
+  rfl
+
 @[simp, mfld_simps]
 theorem symm_source : e.symm.source = e.target :=
   rfl

Mathlib/Topology/Constructions.lean

@@ -538,6 +538,13 @@ theorem Continuous.codRestrict {f : X → Y} {s : Set Y} (hf : Continuous f) (hs
     Continuous (s.codRestrict f hs) :=
   hf.subtype_mk hs
 
+theorem continuous_codRestrict_iff {f : X → Y} {s : Set Y} (hs : ∀ a, f a ∈ s) :
+    Continuous (codRestrict f s hs) ↔ Continuous f := by
+  refine ⟨?_, fun hf ↦ hf.codRestrict hs⟩
+  simp_rw [continuous_def]
+  intro hf t ht
+  exact hf (Subtype.val ⁻¹' t) (isOpen_induced ht)
+
 theorem IsOpenMap.codRestrict {f : X → Y} (hf : IsOpenMap f) {s : Set Y} (hs : ∀ a, f a ∈ s) :
     IsOpenMap (s.codRestrict f hs) :=
   hf.subtype_mk hs

Mathlib/Topology/OpenPartialHomeomorph/Basic.lean

@@ -5,9 +5,9 @@ Authors: Sébastien Gouëzel
 -/
 module
 
-public import Mathlib.Topology.Homeomorph.Lemmas
 public import Mathlib.Topology.OpenPartialHomeomorph.Defs
 public import Mathlib.Topology.Sets.Opens
+public import Mathlib.Topology.PartialHomeomorph.Basic
 /-!
 # Partial homeomorphisms: basic theory
 
@@ -120,17 +120,15 @@ theorem isOpen_image_iff_of_subset_source {s : Set X} (hs : s ⊆ e.source) :
     IsOpen (e '' s) ↔ IsOpen s := by
   rw [← e.symm.isOpen_symm_image_iff_of_subset_target hs, e.symm_symm]
 
-/-- A `PartialEquiv` with continuous open forward map and open source is a
-`OpenPartialHomeomorph`. -/
-@[simps toPartialHomeomorph]
+/-- A `PartialEquiv` which is continuous on its source and has open forward map (on its source)
+and open source is an `OpenPartialHomeomorph`. -/
+@[simps! toPartialHomeomorph]
 def ofContinuousOpenRestrict (e : PartialEquiv X Y) (hc : ContinuousOn e e.source)
     (ho : IsOpenMap (e.source.domRestrict e)) (hs : IsOpen e.source) :
     OpenPartialHomeomorph X Y where
-  toPartialEquiv := e
+  toPartialHomeomorph := PartialHomeomorph.ofContinuousOpenRestrict e hc ho
   open_source := hs
-  open_target := by simpa only [range_domRestrict, e.image_source_eq_target] using ho.isOpen_range
-  continuousOn_toFun := hc
-  continuousOn_invFun := e.image_source_eq_target ▸ ho.continuousOn_image_of_leftInvOn e.leftInvOn
+  open_target := by simpa [e.image_source_eq_target] using ho.isOpen_range
 
 @[simp]
 theorem coe_ofContinuousOpenRestrict (e : PartialEquiv X Y) (hc : ContinuousOn e e.source)
@@ -144,8 +142,8 @@ theorem coe_ofContinuousOpenRestrict_symm (e : PartialEquiv X Y) (hc : Continuou
     ⇑(ofContinuousOpenRestrict e hc ho hs).symm = e.symm :=
   rfl
 
-/-- A `PartialEquiv` with continuous open forward map and open source is a
-`OpenPartialHomeomorph`. -/
+/-- A `PartialEquiv` which is continuous on its source and has open forward map (on its source) and
+open source is an `OpenPartialHomeomorph`. -/
 @[simps! toPartialHomeomorph]
 def ofContinuousOpen (e : PartialEquiv X Y) (hc : ContinuousOn e e.source) (ho : IsOpenMap e)
     (hs : IsOpen e.source) : OpenPartialHomeomorph X Y :=
@@ -165,19 +163,10 @@ theorem coe_ofContinuousOpen_symm (e : PartialEquiv X Y) (hc : ContinuousOn e e.
 
 /-- The homeomorphism obtained by restricting an `OpenPartialHomeomorph` to a subset of the source.
 -/
-@[simps]
+@[simps!]
 def homeomorphOfImageSubsetSource {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : e '' s = t) :
     s ≃ₜ t :=
-  have h₁ : MapsTo e s t := mapsTo_iff_image_subset.2 ht.subset
-  have h₂ : t ⊆ e.target := ht ▸ e.image_source_eq_target ▸ image_mono hs
-  have h₃ : MapsTo e.symm t s := ht ▸ forall_mem_image.2 fun _x hx =>
-      (e.left_inv (hs hx)).symm ▸ hx
-  { toFun := MapsTo.restrict e s t h₁
-    invFun := MapsTo.restrict e.symm t s h₃
-    left_inv := fun a => Subtype.ext (e.left_inv (hs a.2))
-    right_inv := fun b => Subtype.ext <| e.right_inv (h₂ b.2)
-    continuous_toFun := (e.continuousOn.mono hs).mapsToRestrict h₁
-    continuous_invFun := (e.continuousOn_symm.mono h₂).mapsToRestrict h₃ }
+  e.toPartialHomeomorph.homeomorphOfImageSubsetSource hs ht
 
 /-- An open partial homeomorphism defines a homeomorphism between its source and target. -/
 @[simps!]
@@ -197,31 +186,17 @@ theorem nhds_eq_comap_inf_principal {x} (hx : x ∈ e.source) :
 
 /-- If an open partial homeomorphism has source and target equal to univ, then it induces a
 homeomorphism between the whole spaces, expressed in this definition. -/
-@[simps (attr := mfld_simps) -fullyApplied apply symm_apply]
+@[simps! (attr := mfld_simps) -fullyApplied apply symm_apply]
 -- TODO: add a `PartialEquiv` version
 def toHomeomorphOfSourceEqUnivTargetEqUniv (h : e.source = (univ : Set X)) (h' : e.target = univ) :
-    X ≃ₜ Y where
-  toFun := e
-  invFun := e.symm
-  left_inv x :=
-    e.left_inv <| by
-      rw [h]
-      exact mem_univ _
-  right_inv x :=
-    e.right_inv <| by
-      rw [h']
-      exact mem_univ _
-  continuous_toFun := by
-    simpa only [continuousOn_univ, h] using e.continuousOn
-  continuous_invFun := by
-    simpa only [continuousOn_univ, h'] using e.continuousOn_symm
-
-theorem isOpenEmbedding_restrict : IsOpenEmbedding (e.source.domRestrict e) := by
-  refine .of_continuous_injective_isOpenMap (e.continuousOn.comp_continuous
-    continuous_subtype_val Subtype.prop) e.injOn.injective fun V hV ↦ ?_
-  rw [Set.domRestrict_eq, Set.image_comp]
-  exact e.isOpen_image_of_subset_source (e.open_source.isOpenMap_subtype_val V hV)
-    fun _ ⟨x, _, h⟩ ↦ h ▸ x.2
+    X ≃ₜ Y :=
+  e.toPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv h h'
+
+theorem isOpenEmbedding_restrict : IsOpenEmbedding (e.source.domRestrict e) where
+  toIsEmbedding := e.isEmbedding_restrict
+  isOpen_range := by
+    rw [range_domRestrict, image_source_eq_target]
+    exact e.open_target
 
 /-- An open partial homeomorphism whose source is all of `X` defines an open embedding of `X` into
 `Y`. The converse is also true; see `IsOpenEmbedding.toOpenPartialHomeomorph`. -/
@@ -287,7 +262,6 @@ theorem openPartialHomeomorphSubtypeCoe_source :
 @[simp, mfld_simps]
 theorem openPartialHomeomorphSubtypeCoe_target :
     (s.openPartialHomeomorphSubtypeCoe hs).target = s := by
-  simp only [openPartialHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]
-  rfl
+  simp [openPartialHomeomorphSubtypeCoe]
 
 end TopologicalSpace.Opens