prodMk — Mathlib

English

If f: α → β and g: α → γ are Lipschitz with Kf and Kg, then x ↦ (f x, g x) is Lipschitz with 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

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

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