English
If f: α → V and g: α → P are Lipschitz with constants Kf and Kg, then the map x ↦ f(x) +ᵥ g(x) is Lipschitz with constant Kf + Kg.
Русский
Если f: α → V и g: α → P Lipschitz с константами Kf и Kg, то отображение x ↦ f(x) +ᵥ g(x) Lipschitz с константой Kf + Kg.
LaTeX
$$$\operatorname{LipschitzWith}(K_f + K_g)\ (f +ᵥ g)$$$
Lean4
theorem vadd [PseudoEMetricSpace α] {f : α → V} {g : α → P} {Kf Kg : ℝ≥0} (hf : LipschitzWith Kf f)
(hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) (f +ᵥ g) := fun x y =>
calc
edist (f x +ᵥ g x) (f y +ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g y) := edist_vadd_vadd_le _ _ _ _
_ ≤ Kf * edist x y + Kg * edist x y := (add_le_add (hf x y) (hg x y))
_ = (Kf + Kg) * edist x y := (add_mul _ _ _).symm
