accPt_principal_iff_nhdsWithin — Mathlib

English

A point x is an accumulation point of s iff the neighborhood filter restricted to s without x is nontrivial.

Русский

Точка x является накопленной точкой множества s, если фильтр окрестностей x, ограниченный до s без x, не тривиален.

LaTeX

$$$AccPt\ x\ (\mathcal{P} s) \iff \mathcal{N}_{x}^{s \setminus \{x\}} \neq \bot$$

Lean4

theorem accPt_principal_iff_nhdsWithin : AccPt x (𝓟 s) ↔ (𝓝[s \ { x }] x).NeBot := by
  rw [accPt_principal_iff_clusterPt, ClusterPt, nhdsWithin]

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