Mathlib.Topology.ClusterPt

clusterPt_sup theorem

{F G : Filter X} : ClusterPt x (F ⊔ G) ↔ ClusterPt x F ∨ ClusterPt x G

Full source

theorem clusterPt_sup {F G : Filter X} : ClusterPtClusterPt x (F ⊔ G) ↔ ClusterPt x F ∨ ClusterPt x G := by
  simp only [ClusterPt, inf_sup_left, sup_neBot]

Cluster Point Criterion for Filter Supremum: $\text{ClusterPt}_x(F \sqcup G) \leftrightarrow \text{ClusterPt}_x(F) \lor \text{ClusterPt}_x(G)$

Informal description

For any filters $F$ and $G$ on a topological space $X$, a point $x$ is a cluster point of the supremum filter $F \sqcup G$ if and only if $x$ is a cluster point of $F$ or $x$ is a cluster point of $G$.

ClusterPt.neBot theorem

{F : Filter X} (h : ClusterPt x F) : NeBot (𝓝 x ⊓ F)

Full source

theorem ClusterPt.neBot {F : Filter X} (h : ClusterPt x F) : NeBot (𝓝𝓝 x ⊓ F) :=
  h

Non-triviality of Infimum Filter at Cluster Point

Informal description

For any filter $F$ on a topological space $X$, if $x$ is a cluster point of $F$, then the infimum of the neighborhood filter $\mathcal{N}_x$ and $F$ is a non-trivial filter (i.e., it is not equal to the bottom filter $\bot$).

Filter.HasBasis.clusterPt_iff theorem

 {ιX ιF} {pX : ιX → Prop} {sX : ιX → Set X} {pF : ιF → Prop} {sF : ιF → Set X} {F : Filter X}
  (hX : (𝓝 x).HasBasis pX sX) (hF : F.HasBasis pF sF) :
  ClusterPt x F ↔ ∀ ⦃i⦄, pX i → ∀ ⦃j⦄, pF j → (sX i ∩ sF j).Nonempty

Full source

theorem Filter.HasBasis.clusterPt_iff {ιX ιF} {pX : ιX → Prop} {sX : ιX → Set X} {pF : ιF → Prop}
    {sF : ιF → Set X} {F : Filter X} (hX : (𝓝 x).HasBasis pX sX) (hF : F.HasBasis pF sF) :
    ClusterPtClusterPt x F ↔ ∀ ⦃i⦄, pX i → ∀ ⦃j⦄, pF j → (sX i ∩ sF j).Nonempty :=
  hX.inf_basis_neBot_iff hF

Cluster Point Criterion via Filter Bases

Informal description

Let $X$ be a topological space and $F$ a filter on $X$. Suppose the neighborhood filter $\mathcal{N}_x$ has a basis $\{s_X(i) \mid p_X(i)\}$ and $F$ has a basis $\{s_F(j) \mid p_F(j)\}$. Then $x$ is a cluster point of $F$ if and only if for every $i$ with $p_X(i)$ and every $j$ with $p_F(j)$, the intersection $s_X(i) \cap s_F(j)$ is nonempty.

Filter.HasBasis.clusterPt_iff_frequently theorem

 {ι} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : (𝓝 x).HasBasis p s) :
  ClusterPt x F ↔ ∀ i, p i → ∃ᶠ x in F, x ∈ s i

Full source

theorem Filter.HasBasis.clusterPt_iff_frequently {ι} {p : ι → Prop} {s : ι → Set X} {F : Filter X}
    (hx : (𝓝 x).HasBasis p s) : ClusterPtClusterPt x F ↔ ∀ i, p i → ∃ᶠ x in F, x ∈ s i := by
  simp only [hx.clusterPt_iff F.basis_sets, Filter.frequently_iff, inter_comm (s _),
    Set.Nonempty, id, mem_inter_iff]

Cluster Point Criterion via Frequent Membership in Basis Neighborhoods

Informal description

Let $X$ be a topological space and $F$ a filter on $X$. Suppose the neighborhood filter $\mathcal{N}_x$ has a basis $\{s(i) \mid p(i)\}$. Then $x$ is a cluster point of $F$ if and only if for every $i$ with $p(i)$, the set of points $y$ in $F$ that belong to $s(i)$ is frequently nonempty (i.e., $y \in s(i)$ occurs frequently in $F$).

clusterPt_iff_frequently theorem

{F : Filter X} : ClusterPt x F ↔ ∀ s ∈ 𝓝 x, ∃ᶠ y in F, y ∈ s

Full source

theorem clusterPt_iff_frequently {F : Filter X} : ClusterPtClusterPt x F ↔ ∀ s ∈ 𝓝 x, ∃ᶠ y in F, y ∈ s :=
  (𝓝 x).basis_sets.clusterPt_iff_frequently

Cluster Point Criterion via Frequent Membership in Neighborhoods

Informal description

A point $x$ is a cluster point of a filter $F$ on a topological space $X$ if and only if for every neighborhood $s$ of $x$, the set of points $y$ in $F$ that belong to $s$ is frequently nonempty (i.e., $y \in s$ occurs frequently in $F$).

ClusterPt.frequently theorem

{F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ y in 𝓝 x, p y) : ∃ᶠ y in F, p y

Full source

theorem ClusterPt.frequently {F : Filter X} {p : X → Prop} (hx : ClusterPt x F)
    (hp : ∀ᶠ y in 𝓝 x, p y) : ∃ᶠ y in F, p y :=
  clusterPt_iff_frequently.mp hx {y | p y} hp

Frequent Occurrence at Cluster Points

Informal description

Let $F$ be a filter on a topological space $X$, and let $p : X \to \text{Prop}$ be a predicate. If $x$ is a cluster point of $F$ and $p(y)$ holds for all $y$ in some neighborhood of $x$, then there exist infinitely many $y$ in $F$ such that $p(y)$ holds.

clusterPt_iff_nonempty theorem

{F : Filter X} : ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ 𝓝 x → ∀ ⦃V⦄, V ∈ F → (U ∩ V).Nonempty

Full source

theorem clusterPt_iff_nonempty {F : Filter X} :
    ClusterPtClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ 𝓝 x → ∀ ⦃V⦄, V ∈ F → (U ∩ V).Nonempty :=
  inf_neBot_iff

Cluster Point Criterion via Nonempty Intersections

Informal description

A point $x$ is a cluster point of a filter $F$ on a topological space $X$ if and only if for every neighborhood $U$ of $x$ and every set $V$ in $F$, the intersection $U \cap V$ is nonempty.

clusterPt_iff_not_disjoint theorem

{F : Filter X} : ClusterPt x F ↔ ¬Disjoint (𝓝 x) F

Full source

theorem clusterPt_iff_not_disjoint {F : Filter X} :
    ClusterPtClusterPt x F ↔ ¬Disjoint (𝓝 x) F := by
  rw [disjoint_iff, ClusterPt, neBot_iff]

Cluster Point Criterion via Non-Disjoint Filters

Informal description

A point $x$ is a cluster point of a filter $F$ on a topological space $X$ if and only if the neighborhood filter $\mathcal{N}_x$ of $x$ and $F$ are not disjoint, i.e., $\mathcal{N}_x \sqcap F \neq \bot$.

Filter.HasBasis.clusterPt_iff_forall_mem_closure theorem

 {ι} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hF : F.HasBasis p s) : ClusterPt x F ↔ ∀ i, p i → x ∈ closure (s i)

Full source

protected theorem Filter.HasBasis.clusterPt_iff_forall_mem_closure {ι} {p : ι → Prop}
    {s : ι → Set X} {F : Filter X} (hF : F.HasBasis p s) :
    ClusterPtClusterPt x F ↔ ∀ i, p i → x ∈ closure (s i) := by
  simp only [(nhds_basis_opens _).clusterPt_iff hF, mem_closure_iff]
  tauto

Cluster Point Criterion via Basis and Closure

Informal description

Let $X$ be a topological space and $F$ a filter on $X$ with a basis $\{s(i) \mid p(i)\}$ indexed by $\iota$. Then a point $x \in X$ is a cluster point of $F$ if and only if for every index $i$ satisfying $p(i)$, the point $x$ belongs to the closure of $s(i)$. In other words: $$ \text{ClusterPt } x F \leftrightarrow \forall i, p(i) \rightarrow x \in \overline{s(i)} $$

clusterPt_iff_forall_mem_closure theorem

{F : Filter X} : ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s

Full source

theorem clusterPt_iff_forall_mem_closure {F : Filter X} :
    ClusterPtClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s :=
  F.basis_sets.clusterPt_iff_forall_mem_closure

Cluster Point Criterion via Closure of Filter Sets

Informal description

A point $x$ in a topological space $X$ is a cluster point of a filter $F$ on $X$ if and only if for every set $s$ in the filter $F$, the point $x$ belongs to the closure of $s$.

clusterPt_principal_iff theorem

: ClusterPt x (𝓟 s) ↔ ∀ U ∈ 𝓝 x, (U ∩ s).Nonempty

Full source

/-- `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 :
    ClusterPtClusterPt x (𝓟 s) ↔ ∀ U ∈ 𝓝 x, (U ∩ s).Nonempty :=
  inf_principal_neBot_iff

Cluster Point Criterion via Neighborhood Intersection

Informal description

A point $x$ in a topological space is a cluster point of a set $s$ if and only if for every neighborhood $U$ of $x$, the intersection $U \cap s$ is nonempty.

clusterPt_principal_iff_frequently theorem

: ClusterPt x (𝓟 s) ↔ ∃ᶠ y in 𝓝 x, y ∈ s

Full source

theorem clusterPt_principal_iff_frequently :
    ClusterPtClusterPt x (𝓟 s) ↔ ∃ᶠ y in 𝓝 x, y ∈ s := by
  simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, exists_prop, mem_inter_iff]

Cluster Point Criterion for Principal Filter via Frequent Intersection

Informal description

A point $x$ is a cluster point of the principal filter generated by a set $s$ if and only if there exists a point $y$ in every neighborhood of $x$ such that $y \in s$. In other words, $x$ is a cluster point of $\mathcal{P}(s)$ if and only if the set $s$ intersects every neighborhood of $x$ in a nonempty set.

ClusterPt.of_le_nhds theorem

{f : Filter X} (H : f ≤ 𝓝 x) [NeBot f] : ClusterPt x f

Full source

theorem ClusterPt.of_le_nhds {f : Filter X} (H : f ≤ 𝓝 x) [NeBot f] : ClusterPt x f := by
  rwa [ClusterPt, inf_eq_right.mpr H]

Cluster Point Criterion via Neighborhood Filter

Informal description

For any filter $f$ on a topological space $X$, if $f$ is finer than the neighborhood filter $\mathcal{N}_x$ at a point $x \in X$ and $f$ is not the trivial filter, then $x$ is a cluster point of $f$.

ClusterPt.of_le_nhds' theorem

{f : Filter X} (H : f ≤ 𝓝 x) (_hf : NeBot f) : ClusterPt x f

Full source

theorem ClusterPt.of_le_nhds' {f : Filter X} (H : f ≤ 𝓝 x) (_hf : NeBot f) :
    ClusterPt x f :=
  ClusterPt.of_le_nhds H

Cluster Point Criterion via Neighborhood Filter (variant)

Informal description

For any filter $f$ on a topological space $X$, if $f$ is finer than the neighborhood filter $\mathcal{N}_x$ at a point $x \in X$ and $f$ is not the trivial filter, then $x$ is a cluster point of $f$.

ClusterPt.of_nhds_le theorem

{f : Filter X} (H : 𝓝 x ≤ f) : ClusterPt x f

Full source

theorem ClusterPt.of_nhds_le {f : Filter X} (H : 𝓝 x ≤ f) : ClusterPt x f := by
  simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]

Cluster Point Criterion via Neighborhood Filter Inclusion

Informal description

For any filter $f$ on a topological space $X$, if the neighborhood filter $\mathcal{N}_x$ at a point $x \in X$ is less than or equal to $f$, then $x$ is a cluster point of $f$.

ClusterPt.mono theorem

{f g : Filter X} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g

Full source

theorem ClusterPt.mono {f g : Filter X} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g :=
  NeBot.mono H <| inf_le_inf_left _ h

Monotonicity of Cluster Points with Respect to Filter Inclusion

Informal description

For any filters $f$ and $g$ on a topological space $X$, if $x$ is a cluster point of $f$ and $f \leq g$, then $x$ is also a cluster point of $g$.

ClusterPt.of_inf_left theorem

{f g : Filter X} (H : ClusterPt x <| f ⊓ g) : ClusterPt x f

Full source

theorem ClusterPt.of_inf_left {f g : Filter X} (H : ClusterPt x <| f ⊓ g) : ClusterPt x f :=
  H.mono inf_le_left

Cluster Point Preservation Under Infimum Left Factor

Informal description

For any filters $f$ and $g$ on a topological space $X$, if $x$ is a cluster point of the infimum filter $f \sqcap g$, then $x$ is also a cluster point of $f$.

ClusterPt.of_inf_right theorem

{f g : Filter X} (H : ClusterPt x <| f ⊓ g) : ClusterPt x g

Full source

theorem ClusterPt.of_inf_right {f g : Filter X} (H : ClusterPt x <| f ⊓ g) :
    ClusterPt x g :=
  H.mono inf_le_right

Cluster Points from Infimum Filter Imply Cluster Points in Right Filter

Informal description

For any filters $f$ and $g$ on a topological space $X$, if $x$ is a cluster point of the infimum filter $f \sqcap g$, then $x$ is also a cluster point of $g$.

mapClusterPt_def theorem

: MapClusterPt x F u ↔ ClusterPt x (map u F)

Full source

theorem mapClusterPt_def : MapClusterPtMapClusterPt x F u ↔ ClusterPt x (map u F) := Iff.rfl

Characterization of Map Cluster Points via Image Filter

Informal description

A function $u : \alpha \to X$ clusters at a point $x$ along a filter $F$ on $\alpha$ if and only if $x$ is a cluster point of the image filter $u(F)$ on $X$. In other words: $$\text{MapClusterPt}\, x\, F\, u \leftrightarrow \text{ClusterPt}\, x\, (u(F))$$

Filter.EventuallyEq.mapClusterPt_iff theorem

{v : α → X} (h : u =ᶠ[F] v) : MapClusterPt x F u ↔ MapClusterPt x F v

Full source

theorem Filter.EventuallyEq.mapClusterPt_iff {v : α → X} (h : u =ᶠ[F] v) :
    MapClusterPtMapClusterPt x F u ↔ MapClusterPt x F v := by
  simp only [mapClusterPt_def, map_congr h]

Equality of Cluster Points for Eventually Equal Functions

Informal description

Let $u, v : \alpha \to X$ be two functions that are eventually equal along a filter $F$ (i.e., $u =_F v$). Then $u$ clusters at $x$ along $F$ if and only if $v$ clusters at $x$ along $F$. In other words, $\text{MapClusterPt}_x F u \leftrightarrow \text{MapClusterPt}_x F v$.

MapClusterPt.mono theorem

{G : Filter α} (h : MapClusterPt x F u) (hle : F ≤ G) : MapClusterPt x G u

Full source

theorem MapClusterPt.mono {G : Filter α} (h : MapClusterPt x F u) (hle : F ≤ G) :
    MapClusterPt x G u :=
  h.clusterPt.mono (map_mono hle)

Monotonicity of Map Cluster Points with Respect to Filter Inclusion

Informal description

Let $X$ be a topological space, $\alpha$ a type, and $u : \alpha \to X$ a function. If $u$ clusters at $x$ along a filter $F$ on $\alpha$ (i.e., $\text{MapClusterPt}\, x\, F\, u$ holds) and $F \leq G$ for another filter $G$ on $\alpha$, then $u$ also clusters at $x$ along $G$ (i.e., $\text{MapClusterPt}\, x\, G\, u$ holds).

MapClusterPt.tendsto_comp' theorem

 [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Tendsto f (𝓝 x ⊓ map u F) (𝓝 y)) (hu : MapClusterPt x F u) :
  MapClusterPt y F (f ∘ u)

Full source

theorem MapClusterPt.tendsto_comp' [TopologicalSpace Y] {f : X → Y} {y : Y}
    (hf : Tendsto f (𝓝𝓝 x ⊓ map u F) (𝓝 y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u) :=
  (tendsto_inf.2 ⟨hf, tendsto_map.mono_left inf_le_right⟩).neBot (hx := hu)

Cluster Point Preservation under Composition with Tendsto Condition

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a function. Suppose that $f$ tends to $y$ along the filter $\mathcal{N}_x \sqcap \text{map}\, u\, F$, where $\mathcal{N}_x$ is the neighborhood filter at $x$ and $u$ clusters at $x$ along $F$ (i.e., $\text{MapClusterPt}_x F u$ holds). Then the composition $f \circ u$ clusters at $y$ along $F$, i.e., $\text{MapClusterPt}_y F (f \circ u)$ holds.

MapClusterPt.tendsto_comp theorem

 [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Tendsto f (𝓝 x) (𝓝 y)) (hu : MapClusterPt x F u) :
  MapClusterPt y F (f ∘ u)

Full source

theorem MapClusterPt.tendsto_comp [TopologicalSpace Y] {f : X → Y} {y : Y}
    (hf : Tendsto f (𝓝 x) (𝓝 y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u) :=
  hu.tendsto_comp' (hf.mono_left inf_le_left)

Cluster Point Preservation under Continuous Composition

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a function. If $f$ tends to $y$ along the neighborhood filter $\mathcal{N}_x$ at $x$ (i.e., $\lim_{z \to x} f(z) = y$) and $u$ clusters at $x$ along the filter $F$ (i.e., $\text{MapClusterPt}_x F u$ holds), then the composition $f \circ u$ clusters at $y$ along $F$ (i.e., $\text{MapClusterPt}_y F (f \circ u)$ holds).

MapClusterPt.continuousAt_comp theorem

[TopologicalSpace Y] {f : X → Y} (hf : ContinuousAt f x) (hu : MapClusterPt x F u) : MapClusterPt (f x) F (f ∘ u)

Full source

theorem MapClusterPt.continuousAt_comp [TopologicalSpace Y] {f : X → Y} (hf : ContinuousAt f x)
    (hu : MapClusterPt x F u) : MapClusterPt (f x) F (f ∘ u) :=
  hu.tendsto_comp hf

Cluster Point Preservation under Composition with Continuous Function at a Point

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a function continuous at $x \in X$. If $u$ clusters at $x$ along the filter $F$ (i.e., $\text{MapClusterPt}_x F u$ holds), then the composition $f \circ u$ clusters at $f(x)$ along $F$ (i.e., $\text{MapClusterPt}_{f(x)} F (f \circ u)$ holds).

Filter.HasBasis.mapClusterPt_iff_frequently theorem

 {ι : Sort*} {p : ι → Prop} {s : ι → Set X} (hx : (𝓝 x).HasBasis p s) :
  MapClusterPt x F u ↔ ∀ i, p i → ∃ᶠ a in F, u a ∈ s i

Full source

theorem Filter.HasBasis.mapClusterPt_iff_frequently {ι : Sort*} {p : ι → Prop} {s : ι → Set X}
    (hx : (𝓝 x).HasBasis p s) : MapClusterPtMapClusterPt x F u ↔ ∀ i, p i → ∃ᶠ a in F, u a ∈ s i := by
  simp_rw [MapClusterPt, hx.clusterPt_iff_frequently, frequently_map]

Cluster Point Criterion via Neighborhood Basis

Informal description

Let $X$ be a topological space, $x \in X$, and $F$ a filter on some type. Suppose the neighborhood filter $\mathcal{N}_x$ has a basis $\{s_i\}_{i \in \iota}$ indexed by a predicate $p : \iota \to \mathrm{Prop}$. Then a function $u$ clusters at $x$ along $F$ (i.e., $x$ is a cluster point of $u$ with respect to $F$) if and only if for every index $i$ satisfying $p(i)$, the set $\{a \mid u(a) \in s_i\}$ is frequently in $F$.

mapClusterPt_iff_frequently theorem

: MapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ a in F, u a ∈ s

Full source

theorem mapClusterPt_iff_frequently : MapClusterPtMapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ a in F, u a ∈ s :=
  (𝓝 x).basis_sets.mapClusterPt_iff_frequently

Cluster Point Criterion via Neighborhoods

Informal description

A function $u$ clusters at a point $x$ along a filter $F$ if and only if for every neighborhood $s$ of $x$, the set $\{a \mid u(a) \in s\}$ is frequently in $F$.

MapClusterPt.frequently theorem

(h : MapClusterPt x F u) {p : X → Prop} (hp : ∀ᶠ y in 𝓝 x, p y) : ∃ᶠ a in F, p (u a)

Full source

theorem MapClusterPt.frequently (h : MapClusterPt x F u) {p : X → Prop} (hp : ∀ᶠ y in 𝓝 x, p y) :
    ∃ᶠ a in F, p (u a) :=
  h.clusterPt.frequently hp

Frequent Occurrence at Cluster Points of a Function

Informal description

Let $X$ be a topological space, $x \in X$, and $F$ a filter on some type. If a function $u$ clusters at $x$ along $F$ (i.e., $x$ is a cluster point of $u$ with respect to $F$), and a predicate $p : X \to \text{Prop}$ holds for all $y$ in some neighborhood of $x$, then there exist infinitely many $a$ in $F$ such that $p(u(a))$ holds.

mapClusterPt_comp theorem

{φ : α → β} {u : β → X} : MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (map φ F) u

Full source

theorem mapClusterPt_comp {φ : α → β} {u : β → X} :
    MapClusterPtMapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (map φ F) u := Iff.rfl

Cluster Points of Composed Functions and Image Filters

Informal description

For any functions $\phi \colon \alpha \to \beta$ and $u \colon \beta \to X$, the composition $u \circ \phi$ clusters at $x$ along the filter $F$ if and only if $u$ clusters at $x$ along the image filter $\text{map} \, \phi \, F$. In other words, the following equivalence holds: $$ \text{MapClusterPt} \, x \, F \, (u \circ \phi) \leftrightarrow \text{MapClusterPt} \, x \, (\text{map} \, \phi \, F) \, u. $$

Filter.Tendsto.mapClusterPt theorem

[NeBot F] (h : Tendsto u F (𝓝 x)) : MapClusterPt x F u

Full source

theorem Filter.Tendsto.mapClusterPt [NeBot F] (h : Tendsto u F (𝓝 x)) : MapClusterPt x F u :=
  .of_le_nhds h

Cluster Points of Functions Converging to a Point

Informal description

Let $F$ be a non-trivial filter on a topological space $X$ and $u \colon \alpha \to X$ be a function. If $u$ tends to $x$ along $F$ (i.e., $\text{Tendsto} \, u \, F \, (\mathcal{N}_x)$), then $x$ is a cluster point of $u$ along $F$.

MapClusterPt.of_comp theorem

{φ : β → α} {p : Filter β} (h : Tendsto φ p F) (H : MapClusterPt x p (u ∘ φ)) : MapClusterPt x F u

Full source

theorem MapClusterPt.of_comp {φ : β → α} {p : Filter β} (h : Tendsto φ p F)
    (H : MapClusterPt x p (u ∘ φ)) : MapClusterPt x F u :=
  H.clusterPt.mono <| map_mono h

Cluster Points via Composition and Filter Convergence

Informal description

Let $\phi \colon \beta \to \alpha$ be a function and $p$ a filter on $\beta$. If $\phi$ tends to $F$ along $p$ (i.e., $\text{Tendsto} \, \phi \, p \, F$) and $x$ is a cluster point of the composition $u \circ \phi$ along $p$, then $x$ is a cluster point of $u$ along $F$.

accPt_sup theorem

{x : X} {F G : Filter X} : AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G

Full source

theorem accPt_sup {x : X} {F G : Filter X} :
    AccPtAccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G := by
  simp only [AccPt, inf_sup_left, sup_neBot]

Accumulation Points of Filter Suprema: $x \text{ is an accumulation point of } F \sqcup G \iff x \text{ is an accumulation point of } F \text{ or } G$

Informal description

For any point $x$ in a topological space $X$ and any filters $F$ and $G$ on $X$, the following are equivalent: 1. $x$ is an accumulation point of the supremum filter $F \sqcup G$. 2. $x$ is an accumulation point of $F$ or $x$ is an accumulation point of $G$. In other words: $$x \text{ is an accumulation point of } F \sqcup G \iff (x \text{ is an accumulation point of } F) \lor (x \text{ is an accumulation point of } G).$$

accPt_iff_clusterPt theorem

{x : X} {F : Filter X} : AccPt x F ↔ ClusterPt x (𝓟 { x }ᶜ ⊓ F)

Full source

theorem accPt_iff_clusterPt {x : X} {F : Filter X} : AccPtAccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F) := by
  rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]

Characterization of Accumulation Points via Cluster Points

Informal description

For a point $x$ in a topological space $X$ and a filter $F$ on $X$, $x$ is an accumulation point of $F$ if and only if $x$ is a cluster point of the filter obtained by intersecting $F$ with the principal filter of the complement of $\{x\}$. In other words: $$x \text{ is an accumulation point of } F \iff x \text{ is a cluster point of } \mathcal{P}(\{x\}^c) \sqcap F$$

accPt_principal_iff_clusterPt theorem

{x : X} {C : Set X} : AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ { x }))

Full source

/-- `x` is an accumulation point of a set `C` iff it is a cluster point of `C ∖ {x}`. -/
theorem accPt_principal_iff_clusterPt {x : X} {C : Set X} :
    AccPtAccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ { x })) := by
  rw [accPt_iff_clusterPt, inf_principal, inter_comm, diff_eq]

Accumulation Point Characterization via Cluster Points of the Punctured Set

Informal description

For a point $x$ in a topological space $X$ and a subset $C \subseteq X$, $x$ is an accumulation point of $C$ if and only if $x$ is a cluster point of the set $C \setminus \{x\}$. In other words: $$x \text{ is an accumulation point of } C \iff x \text{ is a cluster point of } C \setminus \{x\}.$$

accPt_iff_nhds theorem

{x : X} {C : Set X} : AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Full source

/-- `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_nhds {x : X} {C : Set X} : AccPtAccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by
  simp [accPt_principal_iff_clusterPt, clusterPt_principal_iff, Set.Nonempty, exists_prop,
    and_assoc, @and_comm (¬_ = x)]

Characterization of Accumulation Points via Neighborhoods

Informal description

A point $x$ is an accumulation point of a set $C$ if and only if every neighborhood $U$ of $x$ contains a point $y \in C$ distinct from $x$ (i.e., $y \in U \cap C$ and $y \neq x$).

accPt_iff_frequently theorem

{x : X} {C : Set X} : AccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C

Full source

/-- `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 {x : X} {C : Set X} : AccPtAccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C := by
  simp [accPt_principal_iff_clusterPt, clusterPt_principal_iff_frequently, and_comm]

Accumulation Point Criterion via Frequent Points

Informal description

A point $x$ is an accumulation point of a set $C$ if and only if there are points $y$ in $C$ distinct from $x$ that are frequently in every neighborhood of $x$. In other words, $x$ is an accumulation point of $C$ if and only if for every neighborhood $U$ of $x$, there exists a point $y \in U \cap C$ with $y \neq x$.

accPt_principal_iff_nhdsWithin theorem

: AccPt x (𝓟 s) ↔ (𝓝[s \ { x }] x).NeBot

Full source

theorem accPt_principal_iff_nhdsWithin : AccPtAccPt x (𝓟 s) ↔ (𝓝[s \ {x}] x).NeBot := by
  rw [accPt_principal_iff_clusterPt, ClusterPt, nhdsWithin]

Accumulation Point Criterion via Neighborhood Filter Restriction

Informal description

A point $x$ is an accumulation point of a set $s$ if and only if the neighborhood filter of $x$ restricted to $s \setminus \{x\}$ is non-trivial (i.e., does not contain the empty set).

AccPt.mono theorem

{F G : Filter X} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G

Full source

/-- If `x` is an accumulation point of `F` and `F ≤ G`, then
`x` is an accumulation point of `G`. -/
theorem AccPt.mono {F G : Filter X} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G :=
  NeBot.mono h (inf_le_inf_left _ hFG)

Monotonicity of Accumulation Points with Respect to Filter Inclusion

Informal description

If $x$ is an accumulation point of a filter $F$ and $F \leq G$, then $x$ is also an accumulation point of the filter $G$.

AccPt.clusterPt theorem

{x : X} {F : Filter X} (h : AccPt x F) : ClusterPt x F

Full source

theorem AccPt.clusterPt {x : X} {F : Filter X} (h : AccPt x F) : ClusterPt x F :=
  (accPt_iff_clusterPt.mp h).mono inf_le_right

Accumulation Points are Cluster Points

Informal description

For any point $x$ in a topological space $X$ and any filter $F$ on $X$, if $x$ is an accumulation point of $F$, then $x$ is also a cluster point of $F$.

clusterPt_principal theorem

{x : X} {C : Set X} : ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)

Full source

theorem clusterPt_principal {x : X} {C : Set X} :
    ClusterPtClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C) := by
  constructor
  · intro h
    by_contra! hc
    rw [accPt_principal_iff_clusterPt] at hc
    simp_all only [not_false_eq_true, diff_singleton_eq_self, not_true_eq_false, hc.1]
  · rintro (h | h)
    · exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩
    · exact h.clusterPt

Cluster Point Criterion for Principal Filter: Membership or Accumulation

Informal description

For a point $x$ in a topological space $X$ and a subset $C \subseteq X$, $x$ is a cluster point of the principal filter $\mathcal{P}(C)$ if and only if either $x$ is an element of $C$ or $x$ is an accumulation point of $\mathcal{P}(C)$.

isClosed_setOf_clusterPt theorem

{f : Filter X} : IsClosed {x | ClusterPt x f}

Full source

/-- The set of cluster points of a filter is closed. In particular, the set of limit points
of a sequence is closed. -/
theorem isClosed_setOf_clusterPt {f : Filter X} : IsClosed { x | ClusterPt x f } := by
  simp only [clusterPt_iff_forall_mem_closure, setOf_forall]
  exact isClosed_biInter fun _ _ ↦ isClosed_closure

Closedness of the Set of Cluster Points of a Filter

Informal description

For any filter $f$ on a topological space $X$, the set of cluster points $\{x \mid \text{ClusterPt } x f\}$ is closed.

mem_closure_iff_clusterPt theorem

: x ∈ closure s ↔ ClusterPt x (𝓟 s)

Full source

theorem mem_closure_iff_clusterPt : x ∈ closure sx ∈ closure s ↔ ClusterPt x (𝓟 s) :=
  mem_closure_iff_frequently.trans clusterPt_principal_iff_frequently.symm

Closure Membership via Cluster Points of Principal Filter

Informal description

A point $x$ belongs to the closure of a set $s$ in a topological space if and only if $x$ is a cluster point of the principal filter generated by $s$.

mem_closure_iff_nhds_ne_bot theorem

: x ∈ closure s ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥

Full source

theorem mem_closure_iff_nhds_ne_bot : x ∈ closure sx ∈ closure s ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥ :=
  mem_closure_iff_clusterPt.trans neBot_iff

Closure Membership via Non-Trivial Filter Intersection

Informal description

A point $x$ belongs to the closure of a set $s$ in a topological space if and only if the infimum of the neighborhood filter of $x$ and the principal filter generated by $s$ is not the bottom filter.

mem_closure_iff_nhdsWithin_neBot theorem

: x ∈ closure s ↔ NeBot (𝓝[s] x)

Full source

theorem mem_closure_iff_nhdsWithin_neBot : x ∈ closure sx ∈ closure s ↔ NeBot (𝓝[s] x) :=
  mem_closure_iff_clusterPt

Closure Membership via Non-Trivial Neighborhood Filter Within Set

Informal description

A point $x$ belongs to the closure of a set $s$ in a topological space if and only if the neighborhood filter of $x$ within $s$ is non-trivial (i.e., $\mathcal{N}_s(x) \neq \bot$).

not_mem_closure_iff_nhdsWithin_eq_bot theorem

: x ∉ closure s ↔ 𝓝[s] x = ⊥

Full source

lemma not_mem_closure_iff_nhdsWithin_eq_bot : x ∉ closure sx ∉ closure s ↔ 𝓝[s] x = ⊥ := by
  rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]

Non-membership in Closure via Trivial Neighborhood Filter Within Set

Informal description

A point $x$ does not belong to the closure of a set $s$ in a topological space if and only if the neighborhood filter of $x$ within $s$ is trivial (i.e., $\mathcal{N}_s(x) = \bot$).

dense_compl_singleton theorem

(x : X) [NeBot (𝓝[≠] x)] : Dense ({ x }ᶜ : Set X)

Full source

/-- If `x` is not an isolated point of a topological space, then `{x}ᶜ` is dense in the whole
space. -/
theorem dense_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : Dense ({x}{x}ᶜ : Set X) := by
  intro y
  rcases eq_or_ne y x with (rfl | hne)
  · rwa [mem_closure_iff_nhdsWithin_neBot]
  · exact subset_closure hne

Density of Complement of Non-Isolated Point

Informal description

Let $X$ be a topological space and $x \in X$ be a non-isolated point (i.e., the punctured neighborhood filter $\mathcal{N}_{X\setminus\{x\}}(x)$ is non-trivial). Then the complement of the singleton set $\{x\}$ is dense in $X$.

closure_compl_singleton theorem

(x : X) [NeBot (𝓝[≠] x)] : closure { x }ᶜ = (univ : Set X)

Full source

/-- If `x` is not an isolated point of a topological space, then the closure of `{x}ᶜ` is the whole
space. -/
theorem closure_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : closure {x}{x}ᶜ = (univ : Set X) :=
  (dense_compl_singleton x).closure_eq

Closure of Complement of Non-Isolated Point Equals Whole Space

Informal description

Let $X$ be a topological space and $x \in X$ be a non-isolated point (i.e., the punctured neighborhood filter $\mathcal{N}_{X\setminus\{x\}}(x)$ is non-trivial). Then the closure of the complement of the singleton set $\{x\}$ equals the whole space $X$, i.e., $\overline{\{x\}^c} = X$.

interior_singleton theorem

(x : X) [NeBot (𝓝[≠] x)] : interior { x } = (∅ : Set X)

Full source

/-- If `x` is not an isolated point of a topological space, then the interior of `{x}` is empty. -/
@[simp]
theorem interior_singleton (x : X) [NeBot (𝓝[≠] x)] : interior {x} = (∅ : Set X) :=
  interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x)

Empty Interior of Singleton at Non-Isolated Point

Informal description

Let $X$ be a topological space and $x \in X$ be a non-isolated point (i.e., the punctured neighborhood filter $\mathcal{N}_{X\setminus\{x\}}(x)$ is non-trivial). Then the interior of the singleton set $\{x\}$ is empty, i.e., $\text{int}(\{x\}) = \emptyset$.

not_isOpen_singleton theorem

(x : X) [NeBot (𝓝[≠] x)] : ¬IsOpen ({ x } : Set X)

Full source

theorem not_isOpen_singleton (x : X) [NeBot (𝓝[≠] x)] : ¬IsOpen ({x} : Set X) :=
  dense_compl_singleton_iff_not_open.1 (dense_compl_singleton x)

Non-Isolated Points Have Non-Open Singletons

Informal description

Let $X$ be a topological space and $x \in X$ a non-isolated point (i.e., the punctured neighborhood filter $\mathcal{N}_{X\setminus\{x\}}(x)$ is non-trivial). Then the singleton set $\{x\}$ is not open in $X$.

closure_eq_cluster_pts theorem

: closure s = {a | ClusterPt a (𝓟 s)}

Full source

theorem closure_eq_cluster_pts : closure s = { a | ClusterPt a (𝓟 s) } :=
  Set.ext fun _ => mem_closure_iff_clusterPt

Closure as Set of Cluster Points of Principal Filter

Informal description

The closure of a set $s$ in a topological space is equal to the collection of all points $a$ such that $a$ is a cluster point of the principal filter generated by $s$, i.e., \[ \overline{s} = \{a \mid \text{ClusterPt}\, a\, (\mathcal{P} s)\}. \]

mem_closure_iff_nhds theorem

: x ∈ closure s ↔ ∀ t ∈ 𝓝 x, (t ∩ s).Nonempty

Full source

theorem mem_closure_iff_nhds : x ∈ closure sx ∈ closure s ↔ ∀ t ∈ 𝓝 x, (t ∩ s).Nonempty :=
  mem_closure_iff_clusterPt.trans clusterPt_principal_iff

Closure Membership via Nonempty Neighborhood Intersections

Informal description

A point $x$ belongs to the closure of a set $s$ in a topological space if and only if for every neighborhood $t$ of $x$, the intersection $t \cap s$ is nonempty.

mem_closure_iff_nhds' theorem

: x ∈ closure s ↔ ∀ t ∈ 𝓝 x, ∃ y : s, ↑y ∈ t

Full source

theorem mem_closure_iff_nhds' : x ∈ closure sx ∈ closure s ↔ ∀ t ∈ 𝓝 x, ∃ y : s, ↑y ∈ t := by
  simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]

Characterization of Closure via Neighborhoods and Elements

Informal description

A point $x$ belongs to the closure of a set $s$ in a topological space if and only if for every neighborhood $t$ of $x$, there exists an element $y \in s$ such that $y \in t$.

mem_closure_iff_comap_neBot theorem

: x ∈ closure s ↔ NeBot (comap ((↑) : s → X) (𝓝 x))

Full source

theorem mem_closure_iff_comap_neBot :
    x ∈ closure sx ∈ closure s ↔ NeBot (comap ((↑) : s → X) (𝓝 x)) := by
  simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]

Characterization of closure via non-trivial pullback filter

Informal description

A point $x$ belongs to the closure of a set $s$ in a topological space $X$ if and only if the filter obtained by pulling back the neighborhood filter $\mathcal{N}_x$ along the inclusion map $s \hookrightarrow X$ is not the trivial filter (i.e., it is nonempty and does not contain the empty set).

mem_closure_iff_nhds_basis' theorem

 {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) : x ∈ closure t ↔ ∀ i, p i → (s i ∩ t).Nonempty

Full source

theorem mem_closure_iff_nhds_basis' {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    x ∈ closure tx ∈ closure t ↔ ∀ i, p i → (s i ∩ t).Nonempty :=
  mem_closure_iff_clusterPt.trans <|
    (h.clusterPt_iff (hasBasis_principal _)).trans <| by simp only [exists_prop, forall_const]

Closure Membership Criterion via Neighborhood Basis

Informal description

Let $X$ be a topological space, $x \in X$, and $t \subseteq X$. Suppose the neighborhood filter $\mathcal{N}_x$ has a basis $\{s(i) \mid p(i)\}_{i \in \iota}$. Then $x$ belongs to the closure of $t$ if and only if for every index $i$ satisfying $p(i)$, the intersection $s(i) \cap t$ is nonempty.

mem_closure_iff_nhds_basis theorem

 {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) : x ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i

Full source

theorem mem_closure_iff_nhds_basis {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    x ∈ closure tx ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i :=
  (mem_closure_iff_nhds_basis' h).trans <| by
    simp only [Set.Nonempty, mem_inter_iff, exists_prop, and_comm]

Closure Membership Criterion via Neighborhood Basis Elements

Informal description

Let $X$ be a topological space, $x \in X$, and $t \subseteq X$. Suppose the neighborhood filter $\mathcal{N}_x$ has a basis $\{s(i) \mid p(i)\}_{i \in \iota}$. Then $x$ belongs to the closure of $t$ if and only if for every index $i$ satisfying $p(i)$, there exists an element $y \in t$ such that $y \in s(i)$.

clusterPt_iff_lift'_closure theorem

{F : Filter X} : ClusterPt x F ↔ pure x ≤ (F.lift' closure)

Full source

theorem clusterPt_iff_lift'_closure {F : Filter X} :
    ClusterPtClusterPt x F ↔ pure x ≤ (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]

Characterization of Cluster Points via Closure Lift

Informal description

A point $x$ in a topological space $X$ is a cluster point of a filter $F$ on $X$ if and only if the principal filter $\{x\}$ is contained in the filter generated by taking closures of sets in $F$, i.e., $\{x\} \subseteq F.\text{lift}'(\text{closure})$.

clusterPt_iff_lift'_closure' theorem

{F : Filter X} : ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot

Full source

theorem clusterPt_iff_lift'_closure' {F : Filter X} :
    ClusterPtClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot := by
  rw [clusterPt_iff_lift'_closure, inf_comm]
  constructor
  · intro h
    simp [h, pure_neBot]
  · intro h U hU
    simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h
    simpa using h ({x}{x} ∩ U) ⟨{x}, by simp, U, hU, rfl⟩

Cluster Point Characterization via Nonempty Infimum of Closure Lift and Principal Filter

Informal description

A point $x$ in a topological space $X$ is a cluster point of a filter $F$ on $X$ if and only if the infimum of the filter $F.\text{lift}'(\text{closure})$ (the filter generated by taking closures of sets in $F$) and the principal filter $\{x\}$ is nonempty. In other words, $x$ is a cluster point of $F$ if and only if $F.\text{lift}'(\text{closure}) \sqcap \{x\}$ is nonempty.

clusterPt_lift'_closure_iff theorem

{F : Filter X} : ClusterPt x (F.lift' closure) ↔ ClusterPt x F

Full source

@[simp]
theorem clusterPt_lift'_closure_iff {F : Filter X} :
    ClusterPtClusterPt x (F.lift' closure) ↔ ClusterPt x F := by
  simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)]

Equivalence of Cluster Points under Closure Lift

Informal description

For any filter $F$ on a topological space $X$, a point $x$ is a cluster point of the filter obtained by lifting $F$ with the closure operator if and only if $x$ is a cluster point of $F$ itself. In other words, $\text{ClusterPt}\,x\,(F.\text{lift}'\,\text{closure}) \leftrightarrow \text{ClusterPt}\,x\,F$.

isClosed_iff_clusterPt theorem

: IsClosed s ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s

Full source

theorem isClosed_iff_clusterPt : IsClosedIsClosed s ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s :=
  calc
    IsClosed s ↔ closure s ⊆ s := closure_subset_iff_isClosed.symm
    _ ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s := by simp only [subset_def, mem_closure_iff_clusterPt]

Characterization of Closed Sets via Cluster Points of Principal Filter

Informal description

A subset $s$ of a topological space $X$ is closed if and only if for every point $a \in X$, if $a$ is a cluster point of the principal filter generated by $s$, then $a$ belongs to $s$.

isClosed_iff_nhds theorem

: IsClosed s ↔ ∀ x, (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s

Full source

theorem isClosed_iff_nhds :
    IsClosedIsClosed s ↔ ∀ x, (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s := by
  simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]

Characterization of Closed Sets via Nonempty Neighborhood Intersections

Informal description

A subset $s$ of a topological space $X$ is closed if and only if for every point $x \in X$, whenever every neighborhood $U$ of $x$ intersects $s$ non-trivially (i.e., $U \cap s \neq \emptyset$), then $x$ belongs to $s$.

isClosed_iff_forall_filter theorem

: IsClosed s ↔ ∀ x, ∀ F : Filter X, F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Full source

lemma isClosed_iff_forall_filter :
    IsClosedIsClosed s ↔ ∀ x, ∀ F : Filter X, F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s := by
  simp_rw [isClosed_iff_clusterPt]
  exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
         fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩

Characterization of Closed Sets via Filters

Informal description

A subset $s$ of a topological space $X$ is closed if and only if for every point $x \in X$ and every filter $F$ on $X$ that is nontrivial (i.e., $F$ is not the trivial filter), if $F$ contains all subsets of $s$ (i.e., $F \leq \mathcal{P}(s)$) and $F$ converges to $x$ (i.e., $F \leq \mathcal{N}(x)$), then $x$ belongs to $s$.

mem_closure_of_mem_closure_union theorem

(h : x ∈ closure (s₁ ∪ s₂)) (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂

Full source

theorem mem_closure_of_mem_closure_union (h : x ∈ closure (s₁ ∪ s₂))
    (h₁ : s₁ᶜs₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ := by
  rw [mem_closure_iff_nhds_ne_bot] at *
  rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h

Closure Membership in Union via Neighborhood Condition

Informal description

Let $X$ be a topological space and $s_1, s_2 \subseteq X$. If a point $x$ belongs to the closure of $s_1 \cup s_2$ and the complement of $s_1$ is a neighborhood of $x$, then $x$ belongs to the closure of $s_2$. In other words: $$ x \in \overline{s_1 \cup s_2} \text{ and } s_1^c \in \mathcal{N}(x) \implies x \in \overline{s_2}. $$