English
If for every entourage there exists t ∈ f of small diameter and a point y ∈ t with (x,y) ∈ s, then f converges to x.
Русский
Если для каждого соседа s существует t ∈ f такого малого диаметра и точка y ∈ t так, что (x,y) ∈ s, то f сходится к x.
LaTeX
$$$\text{adhs}: \forall s ∈ 𝓤 α, \exists t ∈ f, t \timesˢ t ⊆ s ∧ ∃ y, (x,y) ∈ s ∧ y ∈ t \Rightarrow f ≤ nhds x$$$
Lean4
/-- The common part of the proofs of `le_nhds_of_cauchy_adhp` and
`SequentiallyComplete.le_nhds_of_seq_tendsto_nhds`: if for any entourage `s`
one can choose a set `t ∈ f` of diameter `s` such that it contains a point `y`
with `(x, y) ∈ s`, then `f` converges to `x`. -/
theorem le_nhds_of_cauchy_adhp_aux {f : Filter α} {x : α}
(adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t) : f ≤ 𝓝 x := by
-- Consider a neighborhood `s` of `x`
intro s hs
rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with
⟨U, U_mem, hU⟩
-- Take a set `t ∈ f`, `t × t ⊆ U`, and a point `y ∈ t` such that `(x, y) ∈ U`
rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩
apply mem_of_superset t_mem
exact fun z hz => hU (prodMk_mem_compRel hxy (ht <| mk_mem_prod hy hz)) rfl
