accPt_iff_clusterPt — Mathlib

English

Accumulation point of F is equivalent to x being a cluster point of the filter 𝓟 {x}ᶜ ⊓ F.

Русский

accum pt x F эквивалентно тому, что x является кластерной точкой фильтра 𝓟 ({x}ᶜ) ⊓ F.

LaTeX

$$$\\mathrm{AccPt}(x,F) \\iff \\mathrm{ClusterPt}(x, \\mathcal{P}\\{x\\}^{c} \\cap F)$$$

Lean4

theorem accPt_iff_clusterPt {x : X} {F : Filter X} : AccPt x F ↔ ClusterPt x (𝓟 { x }ᶜ ⊓ F) := by
  rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]

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