English
For a sequence of entourages V_n, there exists φ strictly increasing such that (u∘f∘φ(n+1), u∘f∘φ(n)) ∈ V_n for all n.
Русский
Для последовательности окружностей V_n существует строго возрастaющая φ, такая что пары принадлежат V_n.
LaTeX
$$$\\exists φ, \\text{StrictMono}(φ) \\land \\forall n, (u(φ(n+1)), u(φ(n))) \\in V_n.$$$
Lean4
theorem subseq_mem_entourage {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α} {a : α}
(hu : Tendsto u atTop (𝓝 a)) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ n, (u <| φ (n + 1), u <| φ n) ∈ V (n + 1) :=
by
rcases mem_atTop_sets.1 (hu (ball_mem_nhds a (symm_le_uniformity <| hV 0))) with ⟨n, hn⟩
rcases (hu.comp (tendsto_add_atTop_nat n)).cauchySeq.subseq_mem fun n => hV (n + 1) with ⟨φ, φ_mono, hφV⟩
exact ⟨fun k => φ k + n, φ_mono.add_const _, hn _ le_add_self, hφV⟩
