comp_lipschitzOnWith — Mathlib

English

If f and g are Lipschitz with constants Kf and Kg, then the map x ↦ (f x, g x) is Lipschitz with constant max(Kf, Kg).

Русский

Если f и g липшицевы с константами Kf и Kg, то отображение x ↦ (f x, g x) липшицево с константой max(Kf, Kg).

LaTeX

$$$\\text{LipschitzWith } (\\max K_f K_g) (\\lambda x, (f x, g x))$$$

Lean4

theorem comp_lipschitzOnWith {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} {s : Set α} (hf : LipschitzWith Kf f)
    (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf * Kg) (f ∘ g) s :=
  lipschitzOnWith_iff_restrict.mpr <| hf.comp hg.to_restrict

Похожие утверждения