prodMk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `f` and `g` are Lipschitz on `s`, so is the induced map `f × g` to the product type. -/
protected theorem prodMk {g : α → γ} {Kf Kg : ℝ≥0} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
    LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s :=
  by
  intro _ hx _ hy
  rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]
  exact max_le_max (hf hx hy) (hg hx hy)

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