feat(Topology): lemmas about nhdsSet filter (leanprover-community#39350)

Author: mcdoll

Mathlib/Order/Filter/Tendsto.lean

@@ -64,6 +64,10 @@ theorem Tendsto.frequently_map {l₁ : Filter α} {l₂ : Filter β} {p : α →
 @[simp]
 theorem tendsto_bot {f : α → β} {l : Filter β} : Tendsto f ⊥ l := by simp [Tendsto]
 
+@[simp]
+theorem tendsto_bot_right_iff {f : α → β} {l : Filter α} : Tendsto f l ⊥ ↔ l = ⊥  := by
+  simp [Tendsto]
+
 theorem Tendsto.of_neBot_imp {f : α → β} {la : Filter α} {lb : Filter β}
     (h : NeBot la → Tendsto f la lb) : Tendsto f la lb := by
   rcases eq_or_neBot la with rfl | hla

Mathlib/Topology/Compactness/Compact.lean

@@ -146,22 +146,39 @@ theorem isCompact_iff_ultrafilter_le_nhds' :
 
 alias ⟨IsCompact.ultrafilter_le_nhds', _⟩ := isCompact_iff_ultrafilter_le_nhds'
 
+/-- If a compact set belongs to a filter and all cluster points in this set and in the filter
+lie in a set `s'` then the filter is less than or equal to `𝓝ˢ s'`. -/
+lemma IsCompact.le_nhdsSet_of_clusterPt (hs : IsCompact s) {l : Filter X} {s' : Set X}
+    (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x ∈ s') : l ≤ 𝓝ˢ s' := by
+  refine le_iff_ultrafilter.2 fun f hf ↦ ?_
+  rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩
+  grw [hx]
+  refine nhds_le_nhdsSet ?_
+  exact h x hxs (.mono (.of_le_nhds hx) hf)
+
 /-- If a compact set belongs to a filter and this filter has a unique cluster point `y` in this set,
 then the filter is less than or equal to `𝓝 y`. -/
 lemma IsCompact.le_nhds_of_unique_clusterPt (hs : IsCompact s) {l : Filter X} {y : X}
     (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x = y) : l ≤ 𝓝 y := by
-  refine le_iff_ultrafilter.2 fun f hf ↦ ?_
-  rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩
-  convert ← hx
-  exact h x hxs (.mono (.of_le_nhds hx) hf)
+  rw [← nhdsSet_singleton]
+  exact hs.le_nhdsSet_of_clusterPt hmem h
+
+/-- If values of `f : Y → X` belong to a compact set `s` eventually along a filter `l`
+and `s'` is the set of `MapClusterPt` for `f` along `l` in `s`,
+then `f` tends to `𝓝ˢ s'` along `l`. -/
+lemma IsCompact.tendsto_nhdsSet_of_mapClusterPt {Y} {l : Filter Y} {s' : Set X} {f : Y → X}
+    (hs : IsCompact s) (hmem : ∀ᶠ x in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x ∈ s') :
+    Tendsto f l (𝓝ˢ s') :=
+  hs.le_nhdsSet_of_clusterPt (mem_map.2 hmem) h
 
 /-- If values of `f : Y → X` belong to a compact set `s` eventually along a filter `l`
 and `y` is a unique `MapClusterPt` for `f` along `l` in `s`,
 then `f` tends to `𝓝 y` along `l`. -/
 lemma IsCompact.tendsto_nhds_of_unique_mapClusterPt {Y} {l : Filter Y} {y : X} {f : Y → X}
     (hs : IsCompact s) (hmem : ∀ᶠ x in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x = y) :
-    Tendsto f l (𝓝 y) :=
-  hs.le_nhds_of_unique_clusterPt (mem_map.2 hmem) h
+    Tendsto f l (𝓝 y) := by
+  rw [← nhdsSet_singleton]
+  exact hs.tendsto_nhdsSet_of_mapClusterPt hmem h
 
 /-- For every open directed cover of a compact set, there exists a single element of the
 cover which itself includes the set. -/

Mathlib/Topology/MetricSpace/Thickening.lean

@@ -672,11 +672,27 @@ theorem frontier_cthickening_disjoint (A : Set α) :
 
 end Cthickening
 
-theorem thickening_ball [PseudoMetricSpace α] (x : α) (ε δ : ℝ) :
+section PseudoMetricSpace
+
+variable {α β E : Type*} [PseudoMetricSpace α] {l : Filter β} {s : Set α}
+
+theorem thickening_ball (x : α) (ε δ : ℝ) :
     thickening ε (ball x δ) ⊆ ball x (ε + δ) := by
   rw [← thickening_singleton, ← thickening_singleton]
   apply thickening_thickening_subset
 
+theorem tendsto_nhdsSet {f : β → α} (hs₁ : IsCompact s) (hs₂ : Set.Nonempty s) :
+    Tendsto f l (𝓝ˢ s) ↔ ∀ ε > 0, ∀ᶠ x in l, infDist (f x) s < ε := by
+  rw [(hasBasis_nhdsSet_thickening hs₁).tendsto_right_iff]
+  congrm (∀ ε hε, ?_)
+  simp [mem_thickening_iff_infDist_lt hs₂]
+
+theorem mem_nhdsSet_iff {t : Set α} (hs : IsCompact s) :
+    t ∈ 𝓝ˢ s ↔ ∃ ε > 0, Metric.thickening ε s ⊆ t := by
+  rw [(hasBasis_nhdsSet_thickening hs).mem_iff]
+
+end PseudoMetricSpace
+
 end Metric
 
 section Clopen

Mathlib/Topology/NhdsSet.lean

@@ -31,7 +31,7 @@ public section
 
 open Set Filter Topology
 
-variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : Filter X}
+variable {α X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : Filter X}
   {s t s₁ s₂ t₁ t₂ : Set X} {x : X}
 
 theorem nhdsSet_diagonal (X) [TopologicalSpace (X × X)] :
@@ -147,6 +147,11 @@ theorem monotone_nhdsSet : Monotone (𝓝ˢ : Set X → Filter X) := fun _ _ =>
 theorem nhds_le_nhdsSet (h : x ∈ s) : 𝓝 x ≤ 𝓝ˢ s :=
   le_sSup <| mem_image_of_mem _ h
 
+theorem tendsto_nhdsSet_of_tendsto_nhds {f : α → X} {l : Filter α} {x : X} (hx : x ∈ s)
+    (hf : Tendsto f l (𝓝 x)) :
+    Tendsto f l (𝓝ˢ s) :=
+  hf.trans (nhds_le_nhdsSet hx)
+
 @[simp]
 theorem nhdsSet_union (s t : Set X) : 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t := by
   simp only [nhdsSet, image_union, sSup_union]