clusterPt_iff — Mathlib

English

For any x in a space X and any ultrafilter f on X, x is a cluster point of f if and only if the principal neighborhood filter 𝓝 x contains f, i.e., f ≤ 𝓝 x.

Русский

Пусть x принадлежит пространству X и f — ультрафильтр на X. Тогда x является кластерной точкой f тогда и только тогда, когда фильтр 𝓝 x включает f, то есть f ≤ 𝓝 x.

LaTeX

$$$\\mathrm{ClusterPt}(x, f) \\iff \\uparrow f \\leq \\mathcal{N}(x)$$$

Lean4

theorem clusterPt_iff {f : Ultrafilter X} : ClusterPt x f ↔ ↑f ≤ 𝓝 x :=
  ⟨f.le_of_inf_neBot', fun h => ClusterPt.of_le_nhds h⟩

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