Theorems · Definition · general topology

ClusterPt

{X : Type u_1} → [TopologicalSpace X] → X → Filter X → Prop

A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊥. Also known as an accumulation point or a limit point, but beware that terminology varies. This is not the same as asking 𝓝[≠] x ⊓ F ≠ ⊥, which is called AccPt in Mathlib. See mem_closure_iff_clusterPt in particular.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

138 results in Mathlib

Foundations

Depth 48 from the axioms, rests on 539 definitions · uses propext, Quot.sound

Assumes

TopologicalSpace