English
Let f be convex on s. For all x, y in s and all z in Icc(x, y), f(z) ≤ max{ f(x), f(y) }.
Русский
Пусть f выпукла на s. Для любых x, y ∈ s и z ∈ Icc(x, y) имеет место f(z) ≤ max{ f(x), f(y) }.
LaTeX
$$$ \operatorname{ConvexOn}(\,\mathbb{K}, s, f) \rightarrow \forall x \in s, \forall y \in s, \forall z \in Icc(x,y),\ f(z) \le \max\{f(x), f(y)\}$$$
Lean4
/-- **Maximum principle** for convex functions on an interval. If a function `f` is convex on the
interval `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`. -/
theorem le_max_of_mem_Icc {s : Set 𝕜} {f : 𝕜 → β} {x y z : 𝕜} (hf : ConvexOn 𝕜 s f) (hx : x ∈ s) (hy : y ∈ s)
(hz : z ∈ Icc x y) : f z ≤ max (f x) (f y) := by rw [← segment_eq_Icc (hz.1.trans hz.2)] at hz;
exact hf.le_max_of_mem_segment hx hy hz
