is_const_of_deriv_eq_zero — Mathlib

English

On a convex set s, if the derivative is bounded in nnnorm by C, then the function is Lipschitz with constant C on s.

Русский

На выпуклом множестве s, если производная ограничена в nnnorm на C, функция Lipschitz с константой C на s.

LaTeX

$$$$ \\text{LipschitzOnWith } C\, f\, s, \\quad C ∈ ℝ_{≥0} $$$$

Lean4

/-- If `f : 𝕜 → G`, `𝕜 = R` or `𝕜 = ℂ`, is differentiable everywhere and its derivative equal zero,
then it is a constant function. -/
theorem _root_.is_const_of_deriv_eq_zero (hf : Differentiable 𝕜 f) (hf' : ∀ x, deriv f x = 0) (x y : 𝕜) : f x = f y :=
  is_const_of_fderiv_eq_zero hf (fun z => by ext; simp [← deriv_fderiv, hf']) _ _

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