le_nhds_iff_adhp_of_cauchy — Mathlib

English

For a Cauchy filter f and x, f ≤ nhds x iff x is a cluster point of f.

Русский

Для Коши-фильтра f и точки x выполняется: f ≤ nhds x эквивалентно тому, что x является кластерной точкой f.

LaTeX

$$$\text{Cauchy}(f) \Rightarrow (f \le nhds x \iff \text{ClusterPt}(x,f))$$$

Lean4

theorem le_nhds_iff_adhp_of_cauchy {f : Filter α} {x : α} (hf : Cauchy f) : f ≤ 𝓝 x ↔ ClusterPt x f :=
  ⟨fun h => ClusterPt.of_le_nhds' h hf.1, le_nhds_of_cauchy_adhp hf⟩

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