English
From a Cauchy sequence with a basis of entourages, one can extract a subsequence φ with strict monotonicity such that (u ∘ φ(n+1), u ∘ φ(n)) ∈ V_n for each n.
Русский
Из Коши-последовательности можно извлечь строго возрастающую подпоследовательность, где пара последующих значений попадает в заданную окружность.
LaTeX
$$$\\exists φ: \\mathbb{N} \\to \\mathbb{N},\\; \\text{StrictMono}(φ) \\land \\forall n, (u(φ(n+1)), u(φ(n))) \\in V_n.$$$
Lean4
theorem subseq_mem {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α} (hu : CauchySeq u) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, (u <| φ (n + 1), u <| φ n) ∈ V n :=
by
have : ∀ n, ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n := fun n =>
by
rw [cauchySeq_iff] at hu
rcases hu _ (hV n) with ⟨N, H⟩
exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩
obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ∀ l ≥ φ n, (u l, u <| φ n) ∈ V n⟩ :=
extraction_forall_of_eventually' this
exact ⟨φ, φ_extr, fun n => hφ _ _ (φ_extr <| Nat.lt_add_one n).le⟩
