exists_is_const_of_deriv_eq_zero — Mathlib

English

If an open set s has a differentiable function with derivative identically zero on s, then the function is constant on s.

Русский

Если на открытом множестве s функция дифференцируема и производная нулевая, то функция константа на s.

LaTeX

$$$$ f|_{s} = c \quad\text{for some constant } c, $$$$

Lean4

theorem _root_.IsOpen.exists_is_const_of_deriv_eq_zero (hs : IsOpen s) (hs' : IsPreconnected s)
    (hf : DifferentiableOn 𝕜 f s) (hf' : s.EqOn (deriv f) 0) : ∃ a, ∀ x ∈ s, f x = a :=
  hs.exists_is_const_of_fderiv_eq_zero hs' hf (fun {x} hx ↦ by ext; simp [← deriv_fderiv, hf' hx])

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