Lemmas on cluster and accumulation points

In this file we prove various lemmas on cluster points (also known as limit points and accumulation points) of a filter and of a sequence.

A filter F on X has x as a cluster point if ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥. A map f : α → X clusters at x along F : Filter α if MapClusterPt x F f : ClusterPt x (map f F). In particular the notion of cluster point of a sequence u is MapClusterPt x atTop u.

theorem clusterPt_sup {X : Type u} [TopologicalSpace X] {x : X} {F G : Filter X} : ClusterPt x (F ⊔ G) ↔ ClusterPt x F ∨ ClusterPt x G

theorem ClusterPt.neBot {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} (h : ClusterPt x F) : (nhds x ⊓ F).NeBot

theorem Filter.HasBasis.clusterPt_iff {X : Type u} [TopologicalSpace X] {x : X} {ιX : Sort u_3} {ιF : Sort u_4} {pX : ιX → Prop} {sX : ιX → Set X} {pF : ιF → Prop} {sF : ιF → Set X} {F : Filter X} (hX : (nhds x).HasBasis pX sX) (hF : F.HasBasis pF sF) : ClusterPt x F ↔ ∀ ⦃i : ιX⦄, pX i → ∀ ⦃j : ιF⦄, pF j → (sX i ∩ sF j).Nonempty

theorem Filter.HasBasis.clusterPt_iff_frequently {X : Type u} [TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : (nhds x).HasBasis p s) : ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in F, x ∈ s i

theorem clusterPt_iff_frequently {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ nhds x, ∃ᶠ (y : X) in F, y ∈ s

theorem ClusterPt.frequently {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (y : X) in F, p y

theorem Filter.HasBasis.clusterPt_iff_frequently' {X : Type u} [TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : F.HasBasis p s) : ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in nhds x, x ∈ s i

theorem clusterPt_iff_frequently' {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ F, ∃ᶠ (y : X) in nhds x, y ∈ s

theorem ClusterPt.frequently' {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ (y : X) in F, p y) : ∃ᶠ (y : X) in nhds x, p y

theorem clusterPt_iff_nonempty {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ nhds x → ∀ ⦃V : Set X⦄, V ∈ F → (U ∩ V).Nonempty

@[deprecated clusterPt_iff_nonempty (since := "2025-03-16")]

theorem clusterPt_iff {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ nhds x → ∀ ⦃V : Set X⦄, V ∈ F → (U ∩ V).Nonempty

Alias of clusterPt_iff_nonempty.

theorem clusterPt_iff_not_disjoint {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ¬Disjoint (nhds x) F

theorem Filter.HasBasis.clusterPt_iff_forall_mem_closure {X : Type u} [TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hF : F.HasBasis p s) : ClusterPt x F ↔ ∀ (i : ι), p i → x ∈ closure (s i)

theorem clusterPt_iff_forall_mem_closure {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s

theorem ClusterPt.mem_closure_of_mem {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F → ∀ s ∈ F, x ∈ closure s

Alias of the forward direction of clusterPt_iff_forall_mem_closure.

theorem clusterPt_principal_iff {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : ClusterPt x (Filter.principal s) ↔ ∀ U ∈ nhds x, (U ∩ s).Nonempty

x is a cluster point of a set s if every neighbourhood of x meets s on a nonempty set. See also mem_closure_iff_clusterPt.

theorem clusterPt_principal_iff_frequently {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : ClusterPt x (Filter.principal s) ↔ ∃ᶠ (y : X) in nhds x, y ∈ s

theorem ClusterPt.of_le_nhds {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} (H : f ≤ nhds x) [f.NeBot] : ClusterPt x f

theorem ClusterPt.of_le_nhds' {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} (H : f ≤ nhds x) (_hf : f.NeBot) : ClusterPt x f

theorem ClusterPt.of_nhds_le {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} (H : nhds x ≤ f) : ClusterPt x f

theorem ClusterPt.mono {X : Type u} [TopologicalSpace X] {x : X} {f g : Filter X} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g

theorem ClusterPt.of_inf_left {X : Type u} [TopologicalSpace X] {x : X} {f g : Filter X} (H : ClusterPt x (f ⊓ g)) : ClusterPt x f

theorem ClusterPt.of_inf_right {X : Type u} [TopologicalSpace X] {x : X} {f g : Filter X} (H : ClusterPt x (f ⊓ g)) : ClusterPt x g

theorem mapClusterPt_def {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u ↔ ClusterPt x (Filter.map u F)

theorem MapClusterPt.clusterPt {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u → ClusterPt x (Filter.map u F)

Alias of the forward direction of mapClusterPt_def.

theorem Filter.EventuallyEq.mapClusterPt_iff {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {v : α → X} (h : u =ᶠ[F] v) : MapClusterPt x F u ↔ MapClusterPt x F v

theorem MapClusterPt.congrFun {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {v : α → X} (h : u =ᶠ[F] v) : MapClusterPt x F u → MapClusterPt x F v

Alias of the forward direction of Filter.EventuallyEq.mapClusterPt_iff.

theorem MapClusterPt.mono {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {G : Filter α} (h : MapClusterPt x F u) (hle : F ≤ G) : MapClusterPt x G u

theorem MapClusterPt.tendsto_comp' {X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (nhds x ⊓ Filter.map u F) (nhds y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u)

theorem MapClusterPt.tendsto_comp {X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (nhds x) (nhds y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u)

theorem MapClusterPt.continuousAt_comp {X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} (hf : ContinuousAt f x) (hu : MapClusterPt x F u) : MapClusterPt (f x) F (f ∘ u)

theorem Filter.HasBasis.mapClusterPt_iff_frequently {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} (hx : (nhds x).HasBasis p s) : MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i

theorem mapClusterPt_iff_frequently {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u ↔ ∀ s ∈ nhds x, ∃ᶠ (a : α) in F, u a ∈ s

@[deprecated mapClusterPt_iff_frequently (since := "2025-03-16")]

theorem mapClusterPt_iff {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u ↔ ∀ s ∈ nhds x, ∃ᶠ (a : α) in F, u a ∈ s

Alias of mapClusterPt_iff_frequently.

theorem MapClusterPt.frequently {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} (h : MapClusterPt x F u) {p : X → Prop} (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (a : α) in F, p (u a)

theorem mapClusterPt_comp {X : Type u} [TopologicalSpace X] {α : Type u_1} {β : Type u_2} {F : Filter α} {x : X} {φ : α → β} {u : β → X} : MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (Filter.map φ F) u

theorem Filter.Tendsto.mapClusterPt {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [F.NeBot] (h : Tendsto u F (nhds x)) : MapClusterPt x F u

theorem MapClusterPt.of_comp {X : Type u} [TopologicalSpace X] {α : Type u_1} {β : Type u_2} {F : Filter α} {u : α → X} {x : X} {φ : β → α} {p : Filter β} (h : Filter.Tendsto φ p F) (H : MapClusterPt x p (u ∘ φ)) : MapClusterPt x F u

theorem accPt_sup {X : Type u} [TopologicalSpace X] {x : X} {F G : Filter X} : AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G

theorem accPt_iff_clusterPt {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : AccPt x F ↔ ClusterPt x (Filter.principal {x}ᶜ ⊓ F)

@[deprecated accPt_iff_clusterPt (since := "2025-04-20")]

theorem acc_iff_cluster {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : AccPt x F ↔ ClusterPt x (Filter.principal {x}ᶜ ⊓ F)

Alias of accPt_iff_clusterPt.

theorem accPt_principal_iff_clusterPt {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ClusterPt x (Filter.principal (C \ {x}))

x is an accumulation point of a set C iff it is a cluster point of C ∖ {x}.

@[deprecated accPt_principal_iff_clusterPt (since := "2025-04-20")]

theorem acc_principal_iff_cluster {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ClusterPt x (Filter.principal (C \ {x}))

Alias of accPt_principal_iff_clusterPt.

---

x is an accumulation point of a set C iff it is a cluster point of C ∖ {x}.

theorem accPt_iff_nhds {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x

x is an accumulation point of a set C iff every neighborhood of x contains a point of C other than x.

theorem accPt_iff_frequently {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhds x, y ≠ x ∧ y ∈ C

x is an accumulation point of a set C iff there are points near x in C and different from x.

theorem accPt_iff_frequently_nhdsNE {X : Type u_3} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhdsWithin x {x}ᶜ, y ∈ C

Variant of accPt_iff_frequently: A point x is an accumulation point of a set C iff points in punctured neighborhoods are frequently contained in C.

theorem accPt_principal_iff_nhdsWithin {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : AccPt x (Filter.principal s) ↔ (nhdsWithin x (s \ {x})).NeBot

theorem AccPt.mono {X : Type u} [TopologicalSpace X] {x : X} {F G : Filter X} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G

If x is an accumulation point of F and F ≤ G, then x is an accumulation point of G.

theorem AccPt.clusterPt {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} (h : AccPt x F) : ClusterPt x F

theorem clusterPt_principal {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : ClusterPt x (Filter.principal C) ↔ x ∈ C ∨ AccPt x (Filter.principal C)

theorem isClosed_setOf_clusterPt {X : Type u} [TopologicalSpace X] {f : Filter X} : IsClosed {x : X | ClusterPt x f}

The set of cluster points of a filter is closed. In particular, the set of limit points of a sequence is closed.

theorem mem_closure_iff_clusterPt {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ClusterPt x (Filter.principal s)

theorem ClusterPt.mem_closure {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : ClusterPt x (Filter.principal s) → x ∈ closure s

Alias of the reverse direction of mem_closure_iff_clusterPt.

theorem mem_closure_iff_nhds_ne_bot {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥

theorem mem_closure_iff_nhdsWithin_neBot {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ (nhdsWithin x s).NeBot

theorem notMem_closure_iff_nhdsWithin_eq_bot {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∉ closure s ↔ nhdsWithin x s = ⊥

@[deprecated notMem_closure_iff_nhdsWithin_eq_bot (since := "2025-05-23")]

theorem not_mem_closure_iff_nhdsWithin_eq_bot {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∉ closure s ↔ nhdsWithin x s = ⊥

Alias of notMem_closure_iff_nhdsWithin_eq_bot.

theorem mem_interior_iff_not_clusterPt_compl {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ interior s ↔ ¬ClusterPt x (Filter.principal sᶜ)

theorem dense_compl_singleton {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : Dense {x}ᶜ

If x is not an isolated point of a topological space, then {x}ᶜ is dense in the whole space.

theorem closure_compl_singleton {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : closure {x}ᶜ = Set.univ

If x is not an isolated point of a topological space, then the closure of {x}ᶜ is the whole space.

@[simp]

theorem interior_singleton {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : interior {x} = ∅

If x is not an isolated point of a topological space, then the interior of {x} is empty.

theorem not_isOpen_singleton {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : ¬IsOpen {x}

theorem closure_eq_cluster_pts {X : Type u} [TopologicalSpace X] {s : Set X} : closure s = {a : X | ClusterPt a (Filter.principal s)}

theorem mem_closure_iff_nhds {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∀ t ∈ nhds x, (t ∩ s).Nonempty

theorem mem_closure_iff_nhds' {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∀ t ∈ nhds x, ∃ (y : ↑s), ↑y ∈ t

theorem mem_closure_iff_comap_neBot {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ (Filter.comap Subtype.val (nhds x)).NeBot

theorem mem_closure_iff_nhds_basis' {X : Type u} [TopologicalSpace X] {ι : Sort w} {x : X} {t : Set X} {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis p s) : x ∈ closure t ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty

theorem mem_closure_iff_nhds_basis {X : Type u} [TopologicalSpace X] {ι : Sort w} {x : X} {t : Set X} {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis p s) : x ∈ closure t ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i

theorem clusterPt_iff_lift'_closure {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ pure x ≤ F.lift' closure

theorem clusterPt_iff_lift'_closure' {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot

@[simp]

theorem clusterPt_lift'_closure_iff {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x (F.lift' closure) ↔ ClusterPt x F

theorem isClosed_iff_clusterPt {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (a : X), ClusterPt a (Filter.principal s) → a ∈ s

theorem isClosed_iff_nhds {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (x : X), (∀ U ∈ nhds x, (U ∩ s).Nonempty) → x ∈ s

theorem isClosed_iff_forall_filter {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ Filter.principal s → F ≤ nhds x → x ∈ s

theorem mem_closure_of_mem_closure_union {X : Type u} [TopologicalSpace X] {x : X} {s₁ s₂ : Set X} (h : x ∈ closure (s₁ ∪ s₂)) (h₁ : s₁ᶜ ∈ nhds x) : x ∈ closure s₂