English
If f: α → P 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: α → P и g: α → P Lipschitz с константами Kf и Kg, то отображение x ↦ f(x) −ᵥ g(x) Lipschitz с константой Kf + Kg.
LaTeX
$$$\operatorname{LipschitzWith}(K_f + K_g)\ (f -ᵥ g)$$$
Lean4
theorem vsub [PseudoEMetricSpace α] {f 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_vsub_vsub_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
