English
If f is convex on a set s, then for any x in s the slope of the secant line through x is monotone on s \\ {x}.
Русский
Если f выпукла на множестве s, то наклон секанты через x в s monotone на s без точки x.
LaTeX
$$$\\forall 𝕜,\\; \\text{ConvexOn } 𝕜\\; s\\; f \\Rightarrow x\\in s \\Rightarrow \\text{MonotoneOn } (\\text{slope } f x)\\ (s \\setminus \\{x\\}).$$
Lean4
/-- If `f : 𝕜 → 𝕜` is convex on `s`, then for any point `x ∈ s` the slope of the secant line of `f`
through `x` is monotone on `s \ {x}`. -/
theorem slope_mono (hfc : ConvexOn 𝕜 s f) (hx : x ∈ s) : MonotoneOn (slope f x) (s \ { x }) :=
(slope_fun_def_field f _).symm ▸ fun _ hy _ hz hz' ↦
hfc.secant_mono hx (mem_of_mem_diff hy) (mem_of_mem_diff hz) (notMem_of_mem_diff hy :) (notMem_of_mem_diff hz :) hz'
