English
If s is convex and the derivative f′ exists within s at every point, and f′(x) ≠ m for all x ∈ s, then either f′(x) < m for all x ∈ s or m < f′(x) for all x ∈ s.
Русский
Если s выпукло и существует производная f′ внутри s на каждой точке, и для всех x ∈ s f′(x) ≠ m, то либо f′(x) < m для всех x ∈ s, либо m < f′(x) для всех x ∈ s.
LaTeX
$$(Convex s) ∧ (∀ x ∈ s, HasDerivWithinAt f (f'(x)) s x) ∧ (∀ x ∈ s, f'(x) ≠ m) ⇒ (∀ x ∈ s, f'(x) < m) ∨ (∀ x ∈ s, m < f'(x))$$
Lean4
/-- If the derivative of a function is never equal to `m`, then either
it is always greater than `m`, or it is always less than `m`. -/
theorem hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne {s : Set ℝ} (hs : Convex ℝ s)
(hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) {m : ℝ} (hf' : ∀ x ∈ s, f' x ≠ m) :
(∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x := by
contrapose! hf'
rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩
exact (hs.ordConnected.image_hasDerivWithinAt hf).out (mem_image_of_mem f' ha) (mem_image_of_mem f' hb) ⟨hma, hmb⟩
