feat(Topology.ProperMap): basic theory of proper maps (#6005)

Mathlib.lean

@@ -3291,6 +3291,7 @@ import Mathlib.Topology.Partial
 import Mathlib.Topology.PartitionOfUnity
 import Mathlib.Topology.PathConnected
 import Mathlib.Topology.Perfect
+import Mathlib.Topology.ProperMap
 import Mathlib.Topology.QuasiSeparated
 import Mathlib.Topology.Semicontinuous
 import Mathlib.Topology.Separation

Mathlib/Order/Filter/Prod.lean

@@ -447,6 +447,12 @@ theorem tendsto_prod_iff {f : α × β → γ} {x : Filter α} {y : Filter β} {
   by simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff_self_iff]
 #align filter.tendsto_prod_iff Filter.tendsto_prod_iff
 
+theorem le_prod {f : Filter (α × β)} {g : Filter α} {g' : Filter β} :
+    (f ≤ g ×ˢ g') ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g' := by
+  dsimp only [SProd.sprod]
+  unfold Filter.prod
+  simp only [le_inf_iff, ← map_le_iff_le_comap, Tendsto]
+
 theorem tendsto_prod_iff' {f : Filter α} {g : Filter β} {g' : Filter γ} {s : α → β × γ} :
     Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).1) f g ∧ Tendsto (fun n => (s n).2) f g' := by
   dsimp only [SProd.sprod]

Mathlib/Topology/Basic.lean

@@ -1356,6 +1356,26 @@ theorem mem_closure_iff_nhds_basis {a : α} {p : ι → Prop} {s : ι → Set α
     simp only [Set.Nonempty, mem_inter_iff, exists_prop, and_comm]
 #align mem_closure_iff_nhds_basis mem_closure_iff_nhds_basis
 
+theorem clusterPt_iff_forall_mem_closure {F : Filter α} {a : α} :
+    ClusterPt a F ↔ ∀ s ∈ F, a ∈ closure s := by
+  simp_rw [ClusterPt, inf_neBot_iff, mem_closure_iff_nhds]
+  rw [forall₂_swap]
+
+theorem clusterPt_iff_lift'_closure {F : Filter α} {a : α} :
+    ClusterPt a F ↔ pure a ≤ (F.lift' closure) := by
+  simp_rw [clusterPt_iff_forall_mem_closure,
+    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
+    exists_const]
+
+theorem clusterPt_iff_lift'_closure' {F : Filter α} {a : α} :
+    ClusterPt a F ↔ (F.lift' closure ⊓ pure a).NeBot := by
+  rw [clusterPt_iff_lift'_closure, ← Ultrafilter.coe_pure, inf_comm, Ultrafilter.inf_neBot_iff]
+
+@[simp]
+theorem clusterPt_lift'_closure_iff {F : Filter α} {a : α} :
+    ClusterPt a (F.lift' closure) ↔ ClusterPt a F := by
+  simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure α) (monotone_closure α)]
+
 /-- `x` belongs to the closure of `s` if and only if some ultrafilter
   supported on `s` converges to `x`. -/
 theorem mem_closure_iff_ultrafilter {s : Set α} {x : α} :
@@ -1752,6 +1772,7 @@ protected theorem Set.MapsTo.closure {s : Set α} {t : Set β} {f : α → β} (
   exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)
 #align set.maps_to.closure Set.MapsTo.closure
 
+/-- See also `IsClosedMap.closure_image_eq_of_continuous`. -/
 theorem image_closure_subset_closure_image {f : α → β} {s : Set α} (h : Continuous f) :
     f '' closure s ⊆ closure (f '' s) :=
   ((mapsTo_image f s).closure h).image_subset

Mathlib/Topology/Filter.lean

@@ -92,6 +92,11 @@ protected theorem HasBasis.nhds {l : Filter α} {p : ι → Prop} {s : ι → Se
   exact h.lift' monotone_principal.Iic
 #align filter.has_basis.nhds Filter.HasBasis.nhds
 
+protected theorem tendsto_pure_self (l : Filter X) :
+    Tendsto (pure : X → Filter X) l (𝓝 l) := by
+  rw [Filter.tendsto_nhds]
+  refine fun s hs ↦ Eventually.mono hs fun x ↦ id
+
 /-- Neighborhoods of a countably generated filter is a countably generated filter. -/
 instance {l : Filter α} [IsCountablyGenerated l] : IsCountablyGenerated (𝓝 l) :=
   let ⟨_b, hb⟩ := l.exists_antitone_basis

Mathlib/Topology/Maps.lean

@@ -538,11 +538,34 @@ 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
 
+/-- A map `f : X → Y` is closed if and only if for all sets `s`, any cluster point of `f '' s` is
+the image by `f` of some cluster point of `s`.
+If you require this for all filters instead of just principal filters, and also that `f` is
+continuous, you get the notion of **proper map**. See `isProperMap_iff_clusterPt`. -/
 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]
 
+theorem IsClosedMap.closure_image_eq_of_continuous [TopologicalSpace α] [TopologicalSpace β]
+    {f : α → β} (f_closed : IsClosedMap f) (f_cont : Continuous f) (s : Set α) :
+    closure (f '' s) = f '' closure s :=
+  subset_antisymm (f_closed.closure_image_subset s) (image_closure_subset_closure_image f_cont)
+
+theorem IsClosedMap.lift'_closure_map_eq [TopologicalSpace α] [TopologicalSpace β]
+    {f : α → β} (f_closed : IsClosedMap f) (f_cont : Continuous f) (F : Filter α) :
+    (map f F).lift' closure = map f (F.lift' closure) := by
+  rw [map_lift'_eq2 (monotone_closure β), map_lift'_eq (monotone_closure α)]
+  congr
+  ext s : 1
+  exact f_closed.closure_image_eq_of_continuous f_cont s
+
+theorem IsClosedMap.mapClusterPt_iff_lift'_closure [TopologicalSpace α] [TopologicalSpace β]
+    {F : Filter α} {f : α → β} (f_closed : IsClosedMap f) (f_cont : Continuous f) {y : β} :
+    MapClusterPt y F f ↔ ((F.lift' closure) ⊓ 𝓟 (f ⁻¹' {y})).NeBot := by
+  rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
+      ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]
+
 section OpenEmbedding
 
 variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
@@ -702,8 +725,7 @@ theorem ClosedEmbedding.comp {g : β → γ} {f : α → β} (hg : ClosedEmbeddi
 
 theorem ClosedEmbedding.closure_image_eq {f : α → β} (hf : ClosedEmbedding f) (s : Set α) :
     closure (f '' s) = f '' closure s :=
-  (hf.isClosedMap.closure_image_subset _).antisymm
-    (image_closure_subset_closure_image hf.continuous)
+  hf.isClosedMap.closure_image_eq_of_continuous hf.continuous s
 #align closed_embedding.closure_image_eq ClosedEmbedding.closure_image_eq
 
 end ClosedEmbedding