English
If a differentiable function has zero derivative everywhere, it is locally constant.
Русский
Если производная нулевая во всех точках, функция локально константна.
LaTeX
$$$f\text{ differentiable on }E\text{ and }f'(x)=0\text{ for all }x\in E\Rightarrow f\text{ is locally constant on }E.$$$
Lean4
/-- If `f` has zero derivative on an open set, then `f` is locally constant on `s`. -/
-- TODO: change the spelling once we have `IsLocallyConstantOn`.
theorem _root_.IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero (hs : IsOpen s) (hf : DifferentiableOn 𝕜 f s)
(hf' : s.EqOn (fderiv 𝕜 f) 0) (t : Set G) : IsOpen (s ∩ f ⁻¹' t) :=
by
refine Metric.isOpen_iff.mpr fun y ⟨hy, hy'⟩ ↦ ?_
obtain ⟨r, hr, h⟩ := Metric.isOpen_iff.mp hs y hy
refine ⟨r, hr, Set.subset_inter h fun x hx ↦ ?_⟩
have := (convex_ball y r).is_const_of_fderivWithin_eq_zero (hf.mono h) ?_ hx (mem_ball_self hr)
· simpa [this]
· intro z hz
simpa only [fderivWithin_of_isOpen Metric.isOpen_ball hz] using hf' (h hz)
