Characterization of basic topological properties in terms of ultrafilters

theorem Ultrafilter.clusterPt_iff {X : Type u} {x : X} [TopologicalSpace X] {f : Ultrafilter X} : ClusterPt x ↑f ↔ ↑f ≤ nhds x

theorem clusterPt_iff_ultrafilter {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} : ClusterPt x f ↔ ∃ (u : Ultrafilter X), ↑u ≤ f ∧ ↑u ≤ nhds x

theorem mapClusterPt_iff_ultrafilter {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {F : Filter α} {u : α → X} : MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), ↑U ≤ F ∧ Filter.Tendsto u (↑U) (nhds x)

theorem isOpen_iff_ultrafilter {X : Type u} {s : Set X} [TopologicalSpace X] : IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ nhds x → s ∈ l

theorem mem_closure_iff_ultrafilter {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ ∃ (u : Ultrafilter X), s ∈ u ∧ ↑u ≤ nhds x

x belongs to the closure of s if and only if some ultrafilter supported on s converges to x.

theorem isClosed_iff_ultrafilter {X : Type u} {s : Set X} [TopologicalSpace X] : IsClosed s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ nhds x → s ∈ u → x ∈ s

theorem continuousAt_iff_ultrafilter {X : Type u} {Y : Type v} {x : X} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : ContinuousAt f x ↔ ∀ (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))

theorem continuous_iff_ultrafilter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))