English
The composition of locally Lipschitz functions is locally Lipschitz.
Русский
Сложение(композиция) локально липшицевых функций сохраняет локальную липшицевость.
LaTeX
$$$\\forall f,g,\\ LocallyLipschitz f \\to \\LocallyLipschitz g \\to \\LocallyLipschitz(f\\circ g)$$$
Lean4
/-- The composition of locally Lipschitz functions is locally Lipschitz. -/
protected theorem comp {f : β → γ} {g : α → β} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
LocallyLipschitz (f ∘ g) := by
intro x
rcases hg x with ⟨Kg, t, ht, hgL⟩
rcases hf (g x) with ⟨Kf, u, hu, hfL⟩
refine ⟨Kf * Kg, t ∩ g ⁻¹' u, inter_mem ht (hg.continuous.continuousAt hu), ?_⟩
exact hfL.comp (hgL.mono inter_subset_left) ((mapsTo_preimage g u).mono_left inter_subset_right)
