locallyLipschitz — Mathlib

English

If f is C^1 at x, then f is strictly differentiable at x with derivative f'.

Русский

Если f является C^1 в точке x, то f имеет строгий производный в x с производной f'.

LaTeX

$$$$\text{ContDiffAt } \Rightarrow \text{HasStrictFDerivAt } f f' x.$$$$

Lean4

/-- If `f` is `C^1`, it is locally Lipschitz. -/
theorem locallyLipschitz {f : E' → F'} (hf : ContDiff 𝕂 1 f) : LocallyLipschitz f :=
  by
  intro x
  rcases hf.contDiffAt.exists_lipschitzOnWith with ⟨K, t, ht, hf⟩
  use K, t

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