English
If f and g are locally Lipschitz, then the map x ↦ (f x, g x) is locally Lipschitz.
Русский
Если f и g локально липшицевы, то отображение x ↦ (f x, g x) локально липшицево.
LaTeX
$$$\\forall f,g,\\ LocallyLipschitz f \\to \\LocallyLipschitz g \\to \\LocallyLipschitz(\\lambda x. (f x, g x))$$$
Lean4
/-- If `f` and `g` are locally Lipschitz, so is the induced map `f × g` to the product type. -/
protected theorem prodMk {f : α → β} (hf : LocallyLipschitz f) {g : α → γ} (hg : LocallyLipschitz g) :
LocallyLipschitz fun x => (f x, g x) := by
intro x
rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩
rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩
refine ⟨max Kf Kg, t₁ ∩ t₂, Filter.inter_mem h₁t h₂t, ?_⟩
exact (hfL.mono inter_subset_left).prodMk (hgL.mono inter_subset_right)
