isLocallyConstant_of_fderiv_eq_zero

English

If a differentiable function has zero Fréchet derivative, then it is constant on connected components inside its domain.

Русский

Если Фреше- производная нулевая, функция константа на компоненте связности области определения.

LaTeX

$$$f\text{ differentiable on }E,\ f'(x)=0\ \forall x,\ then\ f\text{ is constant on connected subsets of }E.$$$

Lean4

theorem _root_.isLocallyConstant_of_fderiv_eq_zero (h₁ : Differentiable 𝕜 f) (h₂ : ∀ x, fderiv 𝕜 f x = 0) :
    IsLocallyConstant f := by
  simpa using isOpen_univ.isOpen_inter_preimage_of_fderiv_eq_zero h₁.differentiableOn fun _ _ ↦ h₂ _

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