English
If a function is differentiable on all of 𝕜 and its derivative is bounded in norm by C across the domain, then the function is Lipschitz with constant C on the whole domain.
Русский
Если функция дифференцируема на всём 𝕜 и её производная ограничена по норме на C, то функция Lipschitz с константой C на всём множестве.
LaTeX
$$$$ \|f(y) - f(x)\| ≤ C \|y - x\|, \quad \forall x,y, $$$$
Lean4
theorem _root_.IsOpen.eqOn_of_deriv_eq {f g : 𝕜 → G} (hs : IsOpen s) (hs' : IsPreconnected s)
(hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) (hf' : s.EqOn (deriv f) (deriv g)) (hx : x ∈ s)
(hfgx : f x = g x) : s.EqOn f g :=
hs.eqOn_of_fderiv_eq hs' hf hg (fun _ hx ↦ ContinuousLinearMap.ext_ring (hf' hx)) hx hfgx
