Mathlib.Topology.Ultrafilter

Ultrafilter.clusterPt_iff theorem

{f : Ultrafilter X} : ClusterPt x f ↔ ↑f ≤ 𝓝 x

Full source

theorem Ultrafilter.clusterPt_iff {f : Ultrafilter X} : ClusterPtClusterPt x f ↔ ↑f ≤ 𝓝 x :=
  ⟨f.le_of_inf_neBot', fun h => ClusterPt.of_le_nhds h⟩

Ultrafilter Cluster Point Criterion: $x$ is a cluster point of $f$ iff $f \leq \mathcal{N}_x$

Informal description

For an ultrafilter $f$ on a topological space $X$ and a point $x \in X$, $x$ is a cluster point of $f$ if and only if the underlying filter of $f$ is less than or equal to the neighborhood filter of $x$.

clusterPt_iff_ultrafilter theorem

{f : Filter X} : ClusterPt x f ↔ ∃ u : Ultrafilter X, u ≤ f ∧ u ≤ 𝓝 x

Full source

theorem clusterPt_iff_ultrafilter {f : Filter X} : ClusterPtClusterPt x f ↔
    ∃ u : Ultrafilter X, u ≤ f ∧ u ≤ 𝓝 x := by
  simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Ultrafilter Characterization of Cluster Points

Informal description

A point $x$ in a topological space $X$ is a cluster point of a filter $f$ if and only if there exists an ultrafilter $u$ on $X$ such that $u$ is finer than $f$ and $u$ converges to $x$ (i.e., $u \leq f$ and $u \leq \mathcal{N}_x$, where $\mathcal{N}_x$ is the neighborhood filter of $x$).

mapClusterPt_iff_ultrafilter theorem

: MapClusterPt x F u ↔ ∃ U : Ultrafilter α, U ≤ F ∧ Tendsto u U (𝓝 x)

Full source

theorem mapClusterPt_iff_ultrafilter :
    MapClusterPtMapClusterPt x F u ↔ ∃ U : Ultrafilter α, U ≤ F ∧ Tendsto u U (𝓝 x) := by
  simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Ultrafilter Characterization of Map Cluster Points

Informal description

For a filter $F$ on a topological space $X$, a point $x \in X$, and a function $u : \alpha \to X$, $x$ is a map cluster point of $u$ with respect to $F$ if and only if there exists an ultrafilter $U$ on $\alpha$ such that $U$ is finer than $F$ and $u$ tends to $x$ along $U$ (i.e., $U \leq F$ and $\text{Tendsto}\, u\, U\, \mathcal{N}_x$, where $\mathcal{N}_x$ is the neighborhood filter of $x$).

isOpen_iff_ultrafilter theorem

: IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l

Full source

theorem isOpen_iff_ultrafilter :
    IsOpenIsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l := by
  simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]

Characterization of Open Sets via Ultrafilters

Informal description

A subset $s$ of a topological space $X$ is open if and only if for every point $x \in s$ and every ultrafilter $l$ on $X$ converging to $x$, the set $s$ belongs to $l$.

mem_closure_iff_ultrafilter theorem

: x ∈ closure s ↔ ∃ u : Ultrafilter X, s ∈ u ∧ ↑u ≤ 𝓝 x

Full source

/-- `x` belongs to the closure of `s` if and only if some ultrafilter
  supported on `s` converges to `x`. -/
theorem mem_closure_iff_ultrafilter :
    x ∈ closure sx ∈ closure s ↔ ∃ u : Ultrafilter X, s ∈ u ∧ ↑u ≤ 𝓝 x := by
  simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]

Ultrafilter Characterization of Closure Membership

Informal description

A point $x$ belongs to the closure of a subset $s$ in a topological space $X$ if and only if there exists an ultrafilter $\mathcal{U}$ on $X$ such that $s \in \mathcal{U}$ and $\mathcal{U}$ converges to $x$ (i.e., $\mathcal{U} \leq \mathcal{N}_x$, where $\mathcal{N}_x$ is the neighborhood filter of $x$).

isClosed_iff_ultrafilter theorem

: IsClosed s ↔ ∀ x, ∀ u : Ultrafilter X, ↑u ≤ 𝓝 x → s ∈ u → x ∈ s

Full source

theorem isClosed_iff_ultrafilter : IsClosedIsClosed s ↔
    ∀ x, ∀ u : Ultrafilter X, ↑u ≤ 𝓝 x → s ∈ u → x ∈ s := by
  simp [isClosed_iff_clusterPt, ClusterPt, ← exists_ultrafilter_iff]

Ultrafilter Characterization of Closed Sets

Informal description

A subset $s$ of a topological space $X$ is closed if and only if for every point $x \in X$ and every ultrafilter $\mathcal{U}$ on $X$ converging to $x$, if $s \in \mathcal{U}$, then $x \in s$.

continuousAt_iff_ultrafilter theorem

: ContinuousAt f x ↔ ∀ g : Ultrafilter X, ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x))

Full source

theorem continuousAt_iff_ultrafilter :
    ContinuousAtContinuousAt f x ↔ ∀ g : Ultrafilter X, ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) :=
  tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))

Ultrafilter Characterization of Continuity at a Point

Informal description

A function $f : X \to Y$ between topological spaces is continuous at a point $x \in X$ if and only if for every ultrafilter $\mathcal{U}$ on $X$ converging to $x$, the image filter $f_* \mathcal{U}$ converges to $f(x)$ in $Y$.

continuous_iff_ultrafilter theorem

: Continuous f ↔ ∀ (x) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x))

Full source

theorem continuous_iff_ultrafilter :
    ContinuousContinuous f ↔ ∀ (x) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) := by
  simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter]

Ultrafilter Characterization of Continuity

Informal description

A function $f \colon X \to Y$ between topological spaces is continuous if and only if for every point $x \in X$ and every ultrafilter $g$ on $X$ converging to $x$, the image filter $f(g)$ converges to $f(x)$ in $Y$.