exists_lipschitzOnWith — Mathlib

English

If f is strictly differentiable at x, then there exists a Lipschitz neighborhood around x with some constant K.

Русский

Если f строго дифференцируема в x, существует окрестность вокруг x на которой f Lipschitz с некоторой константой.

LaTeX

$$$ \\text{HasStrictFDerivAt } f f' x \\Rightarrow \\exists K, \\exists s ∈ 𝓝 x,\\ LipschitzOnWith K\\ f\\ s. $$$

Lean4

/-- If `f` is strictly differentiable at `x` with derivative `f'`, then `f` is Lipschitz in a
neighborhood of `x`. See also `HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt` for a
more precise statement. -/
theorem exists_lipschitzOnWith (hf : HasStrictFDerivAt f f' x) : ∃ K, ∃ s ∈ 𝓝 x, LipschitzOnWith K f s :=
  (exists_gt _).imp hf.exists_lipschitzOnWith_of_nnnorm_lt

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