feat(topology): accumulation in infinite compact sets. (#16862)

src/order/filter/basic.lean

@@ -1791,6 +1791,14 @@ lemma le_comap_map : f ≤ comap m (map m f) := (gc_map_comap m).le_u_l _
 @[simp] lemma comap_bot : comap m ⊥ = ⊥ :=
 bot_unique $ λ s _, ⟨∅, mem_bot, by simp only [empty_subset, preimage_empty]⟩
 
+lemma ne_bot_of_comap (h : (comap m g).ne_bot) : g.ne_bot :=
+begin
+  rw ne_bot_iff at *,
+  contrapose! h,
+  rw h,
+  exact comap_bot
+end
+
 lemma comap_inf_principal_range : comap m (g ⊓ 𝓟 (range m)) = comap m g := by simp
 
 lemma disjoint_comap (h : disjoint g₁ g₂) : disjoint (comap m g₁) (comap m g₂) :=
@@ -2111,6 +2119,13 @@ protected lemma push_pull' (f : α → β) (F : filter α) (G : filter β) :
   map f (comap f G ⊓ F) = G ⊓ map f F :=
 by simp only [filter.push_pull, inf_comm]
 
+lemma principal_eq_map_coe_top (s : set α) : 𝓟 s = map (coe : s → α) ⊤ :=
+by simp
+
+lemma inf_principal_eq_bot_iff_comap {F : filter α} {s : set α} :
+  F ⊓ 𝓟 s = ⊥ ↔ comap (coe : s → α) F = ⊥ :=
+by rw [principal_eq_map_coe_top s, ← filter.push_pull',inf_top_eq, map_eq_bot_iff]
+
 section applicative
 
 lemma singleton_mem_pure {a : α} : {a} ∈ (pure a : filter α) :=

src/topology/basic.lean

@@ -857,8 +857,9 @@ In this section we define [cluster points](https://en.wikipedia.org/wiki/Limit_p
 (also known as limit points and accumulation points) of a filter and of a sequence.
 -/
 
-/-- A point `x` is a cluster point of a filter `F` if 𝓝 x ⊓ F ≠ ⊥. Also known as
-an accumulation point or a limit point. -/
+/-- A point `x` is a cluster point of a filter `F` if `𝓝 x ⊓ F ≠ ⊥`. Also known as
+an accumulation point or a limit point, but beware that terminology varies. This
+is *not* the same as asking `𝓝[≠] x ⊓ F ≠ ⊥`. See `mem_closure_iff_cluster_pt` in particular. -/
 def cluster_pt (x : α) (F : filter α) : Prop := ne_bot (𝓝 x ⊓ F)
 
 lemma cluster_pt.ne_bot {x : α} {F : filter α} (h : cluster_pt x F) : ne_bot (𝓝 x ⊓ F) := h
@@ -874,7 +875,7 @@ lemma cluster_pt_iff {x : α} {F : filter α} :
 inf_ne_bot_iff
 
 /-- `x` is a cluster point of a set `s` if every neighbourhood of `x` meets `s` on a nonempty
-set. -/
+set. See also `mem_closure_iff_cluster_pt`. -/
 lemma cluster_pt_principal_iff {x : α} {s : set α} :
   cluster_pt x (𝓟 s) ↔ ∀ U ∈ 𝓝 x, (U ∩ s).nonempty :=
 inf_principal_ne_bot_iff

src/topology/constructions.lean

@@ -180,6 +180,23 @@ theorem nhds_subtype (s : set α) (a : {x // x ∈ s}) :
   𝓝 a = comap coe (𝓝 (a : α)) :=
 nhds_induced coe a
 
+lemma nhds_within_subtype_eq_bot_iff {s t : set α} {x : s} :
+  𝓝[(coe : s → α) ⁻¹' t] x = ⊥ ↔ 𝓝[t] (x : α) ⊓ 𝓟 s = ⊥ :=
+by rw [inf_principal_eq_bot_iff_comap, nhds_within, nhds_within, comap_inf, comap_principal,
+       nhds_induced]
+
+lemma nhds_ne_subtype_eq_bot_iff {S : set α} {x : S} : 𝓝[{x}ᶜ] x = ⊥ ↔ 𝓝[{x}ᶜ] (x : α) ⊓ 𝓟 S = ⊥ :=
+by rw [← nhds_within_subtype_eq_bot_iff, preimage_compl, ← image_singleton,
+       subtype.coe_injective.preimage_image ]
+
+lemma nhds_ne_subtype_ne_bot_iff {S : set α} {x : S} :
+  (𝓝[{x}ᶜ] x).ne_bot ↔ (𝓝[{x}ᶜ] (x : α) ⊓ 𝓟 S).ne_bot :=
+by rw [ne_bot_iff, ne_bot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]
+
+lemma discrete_topology_subtype_iff {S : set α} :
+  discrete_topology S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥ :=
+by simp_rw [discrete_topology_iff_nhds_ne, set_coe.forall', nhds_ne_subtype_eq_bot_iff]
+
 end topα
 
 /-- A type synonym equiped with the topology whose open sets are the empty set and the sets with

src/topology/order.lean

@@ -327,6 +327,31 @@ lemma singletons_open_iff_discrete {X : Type*} [topological_space X] :
   (∀ a : X, is_open ({a} : set X)) ↔ discrete_topology X :=
 ⟨λ h, ⟨eq_bot_of_singletons_open h⟩, λ a _, @is_open_discrete _ _ a _⟩
 
+/-- This lemma characterizes discrete topological spaces as those whose singletons are
+neighbourhoods. -/
+lemma discrete_topology_iff_nhds [topological_space α] :
+  discrete_topology α ↔ ∀ x : α, 𝓝 x = pure x :=
+begin
+  split ; introI h,
+  { intro x,
+    rw nhds_discrete },
+  { constructor,
+    apply eq_of_nhds_eq_nhds,
+    simp [h, nhds_discrete] },
+end
+
+lemma discrete_topology_iff_nhds_ne [topological_space α] :
+  discrete_topology α ↔ ∀ x : α, 𝓝[≠] x = ⊥ :=
+begin
+  rw discrete_topology_iff_nhds,
+  apply forall_congr (λ x, _),
+  rw [nhds_within, inf_principal_eq_bot, compl_compl],
+  split ; intro h,
+  { rw h,
+    exact singleton_mem_pure },
+  { exact le_antisymm (le_pure_iff.mpr h) (pure_le_nhds x) }
+end
+
 end lattice
 
 section galois_connection

src/topology/separation.lean

@@ -79,13 +79,6 @@ If the space is also compact:
 * `disjoint_nested_nhds`: Given two points `x ≠ y`, we can find neighbourhoods `x ∈ V₁ ⊆ U₁` and
   `y ∈ V₂ ⊆ U₂`, with the `Vₖ` closed and the `Uₖ` open, such that the `Uₖ` are disjoint.
 
-### Discrete spaces
-
-* `discrete_topology_iff_nhds`: Discrete topological spaces are those whose neighbourhood
-  filters are the `pure` filter (which is the principal filter at a singleton).
-* `induced_bot`/`discrete_topology_induced`: The pullback of the discrete topology
-  under an inclusion is the discrete topology.
-
 ## References
 
 https://en.wikipedia.org/wiki/Separation_axiom
@@ -741,20 +734,6 @@ begin
   rw ← induced_compose,
 end
 
-/-- This lemma characterizes discrete topological spaces as those whose singletons are
-neighbourhoods. -/
-lemma discrete_topology_iff_nhds {X : Type*} [topological_space X] :
-  discrete_topology X ↔ (nhds : X → filter X) = pure :=
-begin
-  split,
-  { introI hX,
-    exact nhds_discrete X },
-  { intro h,
-    constructor,
-    apply eq_of_nhds_eq_nhds,
-    simp [h, nhds_bot] }
-end
-
 /-- The topology pulled-back under an inclusion `f : X → Y` from the discrete topology (`⊥`) is the
 discrete topology.
 This version does not assume the choice of a topology on either the source `X`

src/topology/subset_properties.lean

@@ -776,6 +776,15 @@ noncompact_space_of_ne_bot $ by simp only [filter.cocompact_eq_cofinite, filter.
 lemma finite_of_compact_of_discrete [compact_space α] [discrete_topology α] : finite α :=
 finite.of_finite_univ $ compact_univ.finite_of_discrete
 
+lemma exists_nhds_ne_ne_bot (α : Type*) [topological_space α] [compact_space α] [infinite α] :
+  ∃ z : α, (𝓝[≠] z).ne_bot :=
+begin
+  by_contra' H,
+  simp_rw not_ne_bot at H,
+  haveI := discrete_topology_iff_nhds_ne.mpr H,
+  exact infinite.not_finite (finite_of_compact_of_discrete : finite α),
+end
+
 lemma finite_cover_nhds_interior [compact_space α] {U : α → set α} (hU : ∀ x, U x ∈ 𝓝 x) :
   ∃ t : finset α, (⋃ x ∈ t, interior (U x)) = univ :=
 let ⟨t, ht⟩ := compact_univ.elim_finite_subcover (λ x, interior (U x)) (λ x, is_open_interior)
@@ -911,6 +920,17 @@ by rw [compact_iff_compact_in_subtype, image_univ, subtype.range_coe]; refl
 lemma is_compact_iff_compact_space {s : set α} : is_compact s ↔ compact_space s :=
 is_compact_iff_is_compact_univ.trans ⟨λ h, ⟨h⟩, @compact_space.compact_univ _ _⟩
 
+lemma is_compact.finite {s : set α} (hs : is_compact s) (hs' : discrete_topology s) : s.finite :=
+finite_coe_iff.mp (@finite_of_compact_of_discrete _ _ (is_compact_iff_compact_space.mp hs) hs')
+
+lemma exists_nhds_ne_inf_principal_ne_bot {s : set α} (hs : is_compact s) (hs' : s.infinite) :
+  ∃ z ∈ s, (𝓝[≠] z ⊓ 𝓟 s).ne_bot :=
+begin
+  by_contra' H,
+  simp_rw not_ne_bot at H,
+  exact hs' (hs.finite $ discrete_topology_subtype_iff.mpr H),
+end
+
 protected lemma closed_embedding.noncompact_space [noncompact_space α] {f : α → β}
   (hf : closed_embedding f) : noncompact_space β :=
 noncompact_space_of_ne_bot hf.tendsto_cocompact.ne_bot