le_nhds_of_cauchy_adhp — Mathlib

English

If x is an adherent (cluster) point of a Cauchy filter f, then f ≤ nhds x.

Русский

Если x является адгезионной точкой (кластерной) для фильтра f, то f ⊆ nhds x.

LaTeX

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

Lean4

/-- If `x` is an adherent (cluster) point for a Cauchy filter `f`, then it is a limit point
for `f`. -/
theorem le_nhds_of_cauchy_adhp {f : Filter α} {x : α} (hf : Cauchy f) (adhs : ClusterPt x f) : f ≤ 𝓝 x :=
  le_nhds_of_cauchy_adhp_aux
    (fun s hs => by
      obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs
      use t, t_mem, ht
      exact forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem))

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