feat(Topology/Compact): an infinite set has an accumulation point (#9173

)

Add more versions of this statement. Also remove `simp` from `Filter.disjoint_cofinite_{left,right}` as RHS is not much simpler than LHS.

Mathlib/Order/Filter/Cofinite.lean

@@ -65,10 +65,20 @@ theorem cofinite_eq_bot [Finite α] : @cofinite α = ⊥ := cofinite_eq_bot_iff.
 
 theorem frequently_cofinite_iff_infinite {p : α → Prop} :
     (∃ᶠ x in cofinite, p x) ↔ Set.Infinite { x | p x } := by
-  simp only [Filter.Frequently, Filter.Eventually, mem_cofinite, compl_setOf, not_not,
-    Set.Infinite]
+  simp only [Filter.Frequently, eventually_cofinite, not_not, Set.Infinite]
 #align filter.frequently_cofinite_iff_infinite Filter.frequently_cofinite_iff_infinite
 
+lemma frequently_cofinite_mem_iff_infinite {s : Set α} : (∃ᶠ x in cofinite, x ∈ s) ↔ s.Infinite :=
+  frequently_cofinite_iff_infinite
+
+alias ⟨_, _root_.Set.Infinite.frequently_cofinite⟩ := frequently_cofinite_mem_iff_infinite
+
+@[simp]
+lemma cofinite_inf_principal_neBot_iff {s : Set α} : (cofinite ⊓ 𝓟 s).NeBot ↔ s.Infinite :=
+  frequently_mem_iff_neBot.symm.trans frequently_cofinite_mem_iff_infinite
+
+alias ⟨_, _root_.Set.Infinite.cofinite_inf_principal_neBot⟩ := cofinite_inf_principal_neBot_iff
+
 theorem _root_.Set.Finite.compl_mem_cofinite {s : Set α} (hs : s.Finite) : sᶜ ∈ @cofinite α :=
   mem_cofinite.2 <| (compl_compl s).symm ▸ hs
 #align set.finite.compl_mem_cofinite Set.Finite.compl_mem_cofinite
@@ -124,14 +134,10 @@ theorem coprodᵢ_cofinite {α : ι → Type*} [Finite ι] :
 set_option linter.uppercaseLean3 false in
 #align filter.Coprod_cofinite Filter.coprodᵢ_cofinite
 
-@[simp]
 theorem disjoint_cofinite_left : Disjoint cofinite l ↔ ∃ s ∈ l, Set.Finite s := by
-  simp only [hasBasis_cofinite.disjoint_iff l.basis_sets, id, disjoint_compl_left_iff_subset]
-  exact ⟨fun ⟨s, hs, t, ht, hts⟩ => ⟨t, ht, hs.subset hts⟩,
-    fun ⟨s, hs, hsf⟩ => ⟨s, hsf, s, hs, Subset.rfl⟩⟩
+  simp [l.basis_sets.disjoint_iff_right]
 #align filter.disjoint_cofinite_left Filter.disjoint_cofinite_left
 
-@[simp]
 theorem disjoint_cofinite_right : Disjoint l cofinite ↔ ∃ s ∈ l, Set.Finite s :=
   disjoint_comm.trans disjoint_cofinite_left
 #align filter.disjoint_cofinite_right Filter.disjoint_cofinite_right
@@ -152,6 +158,14 @@ end Filter
 
 open Filter
 
+lemma Set.Finite.cofinite_inf_principal_compl {s : Set α} (hs : s.Finite) :
+    cofinite ⊓ 𝓟 sᶜ = cofinite := by
+  simpa using hs.compl_mem_cofinite
+
+lemma Set.Finite.cofinite_inf_principal_diff {s t : Set α} (ht : t.Finite) :
+    cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s := by
+  rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]
+
 /-- For natural numbers the filters `Filter.cofinite` and `Filter.atTop` coincide. -/
 theorem Nat.cofinite_eq_atTop : @cofinite ℕ = atTop := by
   refine' le_antisymm _ atTop_le_cofinite

Mathlib/Topology/Compactness/Compact.lean

@@ -796,12 +796,29 @@ theorem finite_of_compact_of_discrete [CompactSpace X] [DiscreteTopology X] : Fi
   Finite.of_finite_univ <| isCompact_univ.finite_of_discrete
 #align finite_of_compact_of_discrete finite_of_compact_of_discrete
 
+lemma Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact
+    {K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) :
+    ∃ x ∈ K, AccPt x (cofinite ⊓ 𝓟 s) :=
+  (@hK _ hs.cofinite_inf_principal_neBot (inf_le_right.trans <| principal_mono.2 hsub)).imp
+    fun x hx ↦ by rwa [acc_iff_cluster, inf_comm, inf_right_comm,
+      (finite_singleton _).cofinite_inf_principal_compl]
+
+lemma Set.Infinite.exists_accPt_of_subset_isCompact {K : Set X} (hs : s.Infinite)
+    (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (𝓟 s) :=
+  let ⟨x, hxK, hx⟩ := hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact hK hsub
+  ⟨x, hxK, hx.mono inf_le_right⟩
+
+lemma Set.Infinite.exists_accPt_cofinite_inf_principal [CompactSpace X] (hs : s.Infinite) :
+    ∃ x, AccPt x (cofinite ⊓ 𝓟 s) := by
+  simpa only [mem_univ, true_and]
+    using hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact isCompact_univ s.subset_univ
+
+lemma Set.Infinite.exists_accPt_principal [CompactSpace X] (hs : s.Infinite) : ∃ x, AccPt x (𝓟 s) :=
+  hs.exists_accPt_cofinite_inf_principal.imp fun _x hx ↦ hx.mono inf_le_right
+
 theorem exists_nhds_ne_neBot (X : Type*) [TopologicalSpace X] [CompactSpace X] [Infinite X] :
-    ∃ x : X, (𝓝[≠] x).NeBot := by
-  by_contra! H
-  simp_rw [not_neBot] at H
-  haveI := discreteTopology_iff_nhds_ne.2 H
-  exact Infinite.not_finite (finite_of_compact_of_discrete : Finite X)
+    ∃ z : X, (𝓝[≠] z).NeBot := by
+  simpa [AccPt] using (@infinite_univ X _).exists_accPt_principal
 #align exists_nhds_ne_ne_bot exists_nhds_ne_neBot
 
 theorem finite_cover_nhds_interior [CompactSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
@@ -937,10 +954,8 @@ theorem IsCompact.finite (hs : IsCompact s) (hs' : DiscreteTopology s) : s.Finit
 #align is_compact.finite IsCompact.finite
 
 theorem exists_nhds_ne_inf_principal_neBot (hs : IsCompact s) (hs' : s.Infinite) :
-    ∃ x ∈ s, (𝓝[≠] x ⊓ 𝓟 s).NeBot := by
-  by_contra! H
-  simp_rw [not_neBot] at H
-  exact hs' (hs.finite <| discreteTopology_subtype_iff.mpr H)
+    ∃ z ∈ s, (𝓝[≠] z ⊓ 𝓟 s).NeBot :=
+  hs'.exists_accPt_of_subset_isCompact hs Subset.rfl
 #align exists_nhds_ne_inf_principal_ne_bot exists_nhds_ne_inf_principal_neBot
 
 protected theorem ClosedEmbedding.noncompactSpace [NoncompactSpace X] {f : X → Y}