English
If f is Lipschitz with constant K, then f preserves Cauchy sequences: the image of a Cauchy sequence under f is Cauchy.
Русский
Если f - липшицева с константой K, то отображение сохраняет последовательности Коши: образ Кошевой последовательности под действием f также Коши.
LaTeX
$$$ \\operatorname{LipschitzWith}(K,f) \\Rightarrow \\forall u:\\\\mathbb{N} \\to \\alpha, \\ \\operatorname{CauchySeq}(u) \\Rightarrow \\operatorname{CauchySeq}(f \\circ u) $$$
Lean4
theorem cauchySeq_comp {f : α → β} (hf : LipschitzWith K f) {u : ℕ → α} (hu : CauchySeq u) : CauchySeq (f ∘ u) :=
by
rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
· exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)
· exact fun n m N hn hm ↦ hf.dist_le_mul_of_le (hb n m N hn hm)
· rw [← mul_zero (K : ℝ)]
exact blim.const_mul _
