English
If a function between normed spaces is differentiable and its Fréchet derivative is identically zero on a connected domain, then the function is constant on that domain.
Русский
Если функция между нормированными пространствами гладкая и ее производная Фреше равна нулю на связной области, то функция постоянна на этой области.
LaTeX
$$$[Differentiable 𝕜 f] \\\\land [∀ x, fderiv 𝕜 f x = 0] \\\\Rightarrow f(x) = f(y) \\,\\text{ for all } x,y$$$
Lean4
theorem _root_.is_const_of_fderiv_eq_zero {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → G}
(hf : Differentiable 𝕜 f) (hf' : ∀ x, fderiv 𝕜 f x = 0) (x y : E) : f x = f y :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
let A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
exact
convex_univ.is_const_of_fderivWithin_eq_zero hf.differentiableOn (fun x _ => by rw [fderivWithin_univ]; exact hf' x)
trivial trivial
