English
If s is a set and a Lipschitz-on-with f on s with range in s, then f sends Cauchy sequences in any ambient space to Cauchy sequences.
Русский
Если f липшицева на подмножестве s и множество значений в s, то образ Кошевой последовательности сохраняется.
LaTeX
$$$ {s : Set\\alpha} \\; {f : \\alpha \\to \\beta} \\; (hf : LipschitzOnWith\\ K\\ f\\ s) \\Rightarrow \\forall u:\\\\mathbb{N} \\to \\alpha, \\operatorname{CauchySeq}(u) \\Rightarrow \\operatorname{CauchySeq}(f \\circ u) $$$
Lean4
theorem cauchySeq_comp {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) {u : ℕ → α} (hu : CauchySeq u)
(h'u : range u ⊆ s) : 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)
· intro n m N hn hm
have A n : u n ∈ s := h'u (mem_range_self _)
apply (hf.dist_le_mul _ (A n) _ (A m)).trans
exact mul_le_mul_of_nonneg_left (hb n m N hn hm) K.2
· rw [← mul_zero (K : ℝ)]
exact blim.const_mul _
