English
Let f be concave on s. For all x, y in s and z in Icc(x, y), min{ f(x), f(y) } ≤ f(z).
Русский
Пусть f вогнута на s. Тогда для любых x, y ∈ s и z ∈ Icc(x, y) верно min{ f(x), f(y) } ≤ f(z).
LaTeX
$$$ \operatorname{ConcaveOn}(\,\mathbb{K}, s, f) \rightarrow \forall x \in s, \forall y \in s, \forall z \in Icc(x,y),\ \min\{f(x), f(y)\} \le f(z)$$$
Lean4
/-- **Minimum principle** for concave functions on an interval. If a function `f` is concave on the
interval `[x, y]`, then the eventual minimum of `f` on `[x, y]` is at `x` or `y`. -/
theorem min_le_of_mem_Icc {s : Set 𝕜} {f : 𝕜 → β} {x y z : 𝕜} (hf : ConcaveOn 𝕜 s f) (hx : x ∈ s) (hy : y ∈ s)
(hz : z ∈ Icc x y) : min (f x) (f y) ≤ f z :=
hf.dual.le_max_of_mem_Icc hx hy hz
