ClusterPt — Mathlib

English

A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊥.

Русский

Точка x является кластерной точкой фильтра F, если 𝓝 x ⊓ F ≠ ⊥.

LaTeX

$$$\operatorname{ClusterPt}(x,F) \iff 𝓝 x \nabla F \ne \bot$$$

Lean4

/-- 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. -/
def ClusterPt (x : X) (F : Filter X) : Prop :=
  NeBot (𝓝 x ⊓ F)

Похожие утверждения