Limit_Point_iff_Superfilter_Converges
Provedfiltersproofwikitopology
A point x is a limit point (cluster point) of a filter F iff there exists a filter finer than F converging to x.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Limit_Point_iff_Superfilter_Converges {α : Type _} [TopologicalSpace α] (F : Filter α) (x : α) : ClusterPt x F ↔ ∃ G : Filter α, G ≠ ⊥ ∧ G ≤ F ∧ G ≤ nhds x := by sorrySource