English
If f is convex on s, and f(x) < f(z) with z on the segment between x and y, then f(z) < f(y).
Русский
Если f выпукла на s и f(x) < f(z) при z на отрезке между x и y, то f(z) < f(y).
LaTeX
$$$\ConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s, z\in openSegment(\mathfrak{K}, x, y): f(x) < f(z) \Rightarrow f(z) < f(y)$$$
Lean4
theorem lt_left_of_right_lt (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y)
(hyz : f y < f z) : f z < f x := by
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
exact hf.lt_left_of_right_lt' hx hy ha hb hab hyz