feat(Topology.Constructions): restriction of a closed map (#6013)

leanprover-community · Jul 21, 2023 · 88fb181 · 88fb181
1 parent ef85ff8
commit 88fb181
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 0 deletions.
diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
@@ -350,6 +350,10 @@ def MapsTo.restrict (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t)
   Subtype.map f h
 #align set.maps_to.restrict Set.MapsTo.restrict
 
+theorem MapsTo.restrict_commutes (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) :
+    Subtype.val ∘ h.restrict f s t = f ∘ Subtype.val :=
+  rfl
+
 @[simp]
 theorem MapsTo.val_restrict_apply (h : MapsTo f s t) (x : s) : (h.restrict f s t x : β) = f x :=
   rfl

diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean
@@ -1030,6 +1030,17 @@ theorem IsOpenMap.restrict {f : α → β} (hf : IsOpenMap f) {s : Set α} (hs :
   hf.comp hs.isOpenMap_subtype_val
 #align is_open_map.restrict IsOpenMap.restrict
 
+lemma IsClosedMap.restrictPreimage {f : α → β} (hcl : IsClosedMap f) (T : Set β) :
+    IsClosedMap (T.restrictPreimage f) := by
+  rw [isClosedMap_iff_clusterPt] at hcl ⊢
+  intro A ⟨y, hyT⟩ hy
+  rw [restrictPreimage, MapClusterPt, ← inducing_subtype_val.mapClusterPt_iff, MapClusterPt,
+      map_map, MapsTo.restrict_commutes, ← map_map, ← MapClusterPt, map_principal] at hy
+  rcases hcl _ y hy with ⟨x, hxy, hx⟩
+  have hxT : f x ∈ T := hxy ▸ hyT
+  refine ⟨⟨x, hxT⟩, Subtype.ext hxy, ?_⟩
+  rwa [← inducing_subtype_val.mapClusterPt_iff, MapClusterPt, map_principal]
+
 nonrec theorem IsClosed.closedEmbedding_subtype_val {s : Set α} (hs : IsClosed s) :
     ClosedEmbedding ((↑) : s → α) :=
   closedEmbedding_subtype_val hs

diff --git a/Mathlib/Topology/Maps.lean b/Mathlib/Topology/Maps.lean
@@ -538,6 +538,11 @@ theorem isClosedMap_iff_closure_image [TopologicalSpace α] [TopologicalSpace β
         _ = f '' c := by rw [hc.closure_eq]⟩
 #align is_closed_map_iff_closure_image isClosedMap_iff_closure_image
 
+theorem isClosedMap_iff_clusterPt [TopologicalSpace α] [TopologicalSpace β] {f : α → β} :
+    IsClosedMap f ↔ ∀ s y, MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s) := by
+  simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt,
+    and_comm]
+
 section OpenEmbedding
 
 variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]