exists_lipschitzOnWith — Mathlib

English

If f is C^1 around x, then there exists a neighborhood where f is Lipschitz.

Русский

Если f является C^1 вокруг x, то существует окрестность, на которой f липшицова.

LaTeX

$$$$\exists K, \exists t \in \mathcal{N}(x), \text{LipschitzOnWith } K\ f\ t.$$$$

Lean4

/-- If `f` is `C^1` at `x`, then `f` is Lipschitz in a neighborhood of `x`. -/
theorem exists_lipschitzOnWith {f : E' → F'} {x : E'} (hf : ContDiffAt 𝕂 1 f x) :
    ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t :=
  (hf.hasStrictFDerivAt le_rfl).exists_lipschitzOnWith

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