English
If there is a family of entourages U_n that control the proximity of f(m) and f(n), and U_n refine all entourages, then f is Cauchy.
Русский
Если есть управление близости через семейство окружностей U_n, которые уточняют все окружности, то f — Коши.
LaTeX
$$$(\\forall s \\in 𝓤 α)(\\exists n, U_n \\subseteq s)\\; \\Rightarrow \\ ; (hf) \\Rightarrow \\ CauchySeq(f).$$$
Lean4
/-- Any shift of a Cauchy sequence is also a Cauchy sequence. -/
theorem cauchySeq_shift {u : ℕ → α} (k : ℕ) : CauchySeq (fun n ↦ u (n + k)) ↔ CauchySeq u :=
by
constructor <;> intro h
· rw [cauchySeq_iff] at h ⊢
intro V mV
obtain ⟨N, h⟩ := h V mV
use N + k
intro a ha b hb
convert h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> omega
· exact h.comp_tendsto (tendsto_add_atTop_nat k)
