of_nhds_le — Mathlib

English

If x is a cluster point of f and f ≤ g, then x is a cluster point of g.

Русский

Если x является кластерной точкой фильтра f и f ≤ g, то x является кластерной точкой фильтра g.

LaTeX

$$$\\mathrm{ClusterPt}(x,f) \\to\\, (f \\le g) \\Rightarrow \\mathrm{ClusterPt}(x,g)$$$

Lean4

theorem of_nhds_le {f : Filter X} (H : 𝓝 x ≤ f) : ClusterPt x f := by
  simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]

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