English
If u is CauchySeq and V_n is a sequence of entourages, we can extract a strictly increasing φ such that (u∘f∘φ(n), u∘g∘φ(n)) ∈ V_n for all n.
Русский
Если есть КошиSeq u и последовательность окружностей V_n, то можно выбрать строго возрастающую φ так, что пары (u∘f∘φ(n), u∘g∘φ(n)) попадают в V_n.
LaTeX
$$$\\exists \\phi:\\mathbb{N}\\to\\mathbb{N},\\ \\text{StrictMono}(\\phi) \\land \\forall n, (u(f(\\phi(n))), u(g(\\phi(n)))) \\in V_n.$$$
Lean4
theorem subseq_subseq_mem {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α} (hu : CauchySeq u) {f g : ℕ → ℕ}
(hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n :=
by
rw [cauchySeq_iff_tendsto] at hu
exact ((hu.comp <| hf.prod_atTop hg).comp tendsto_atTop_diagonal).subseq_mem hV
