English
If s is open and preconnected, and f is differentiable on s with zero derivative there, then f is constant on s.
Русский
Если s открыто и предварительно связно, и f гладкая на s с нулевой производной на s, то f постоянна на s.
LaTeX
$$$IsOpen s \\Rightarrow IsPreconnected s \\Rightarrow DifferentiableOn 𝕜 f s \\Rightarrow s.EqOn (fderiv 𝕜 f) 0 s \\Rightarrow \\exists a, \\forall x \\in s, f x = a$$$
Lean4
/-- If `f` has zero derivative on a connected open set, then `f` is constant on `s`. -/
theorem _root_.IsOpen.exists_is_const_of_fderiv_eq_zero (hs : IsOpen s) (hs' : IsPreconnected s)
(hf : DifferentiableOn 𝕜 f s) (hf' : s.EqOn (fderiv 𝕜 f) 0) : ∃ a, ∀ x ∈ s, f x = a :=
by
obtain (rfl | ⟨y, hy⟩) := s.eq_empty_or_nonempty
· exact ⟨0, by simp⟩
· refine ⟨f y, fun x hx ↦ ?_⟩
have h₁ := hs.isOpen_inter_preimage_of_fderiv_eq_zero hf hf' {f y}
have h₂ := hf.continuousOn.comp_continuous continuous_subtype_val (fun x ↦ x.2)
by_contra h₃
obtain ⟨t, ht, ht'⟩ := (isClosed_singleton (x := f y)).preimage h₂
have ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y := by simpa [Set.ext_iff] using ht'
obtain ⟨z, H₁, H₂, H₃⟩ :=
hs' _ _ h₁ ht (fun x h ↦ by simp [h, ht'', eq_or_ne]) ⟨y, by simpa⟩ ⟨x, by simp [ht'' _ hx, hx, h₃]⟩
exact (ht'' _ H₁).mp H₃ H₂.2
