isOpen_inter_preimage_of_deriv_eq_zero

English

If a function is differentiable on a domain and its derivative is zero everywhere, then the function is constant on the domain.

Русский

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

LaTeX

$$$$ f(x) = f(y), \quad \forall x,y \text{ in domain}, $$$$

Lean4

theorem _root_.IsOpen.isOpen_inter_preimage_of_deriv_eq_zero (hs : IsOpen s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (deriv f) 0) (t : Set G) : IsOpen (s ∩ f ⁻¹' t) :=
  hs.isOpen_inter_preimage_of_fderiv_eq_zero hf (fun x hx ↦ by ext; simp [← deriv_fderiv, hf' hx]) t

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