English
A strictly convex function on an open segment is strictly bounded above by the maximum of its endpoints on interior points of the segment.
Русский
Строго выпуклая функция на открытом отрезке имеет строгое верхнее ограничение над концами отрезка на внутренних точках.
LaTeX
$$$\StrictConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s, x\neq y, z\in openSegment(\mathfrak{K}, x, y): f(z) < \max\{f(x), f(y)\}$$$
Lean4
/-- A strictly convex function on an open segment is strictly upper-bounded by the max of its
endpoints. -/
theorem lt_on_openSegment (hf : StrictConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
(hz : z ∈ openSegment 𝕜 x y) : f z < max (f x) (f y) :=
let ⟨_, _, ha, hb, hab, hz⟩ := hz
hz ▸ hf.lt_on_open_segment' hx hy hxy ha hb hab
