of_le_nhds — Mathlib

English

If f is a filter on X with f ≤ nhds(x) and f is not the bottom filter, then x is a cluster point of f.

Русский

Пусть f — фильтр на X с f ≤ nhds(x) и f не тождественный нулю; тогда x является кластерной точкой фильтра f.

LaTeX

$$$f \\le \\mathcal{N}(x) \\quad\\Rightarrow\\quad \\mathrm{ClusterPt}(x,f)\\quad(\\text{при } f\\neq\\bot)$$$

Lean4

theorem of_le_nhds {f : Filter X} (H : f ≤ 𝓝 x) [NeBot f] : ClusterPt x f := by rwa [ClusterPt, inf_eq_right.mpr H]

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