exists_le_of_mem_convexHull — Mathlib

English

Among the values on the convex hull of a finite set, the maximum can be found at some point of the set.

Русский

Из значений на выпуклой оболочке конечного множества максимум достигается в одной из точек множества.

LaTeX

$$$ \text{ConvexOn}_{\mathbb{K}}(s,f) \Rightarrow \exists i, f(p_i) \ge f(x) \text{ for some } x \in \text{convexHull}(t)$$$

Lean4

/-- **Minimum principle** for concave functions. If a function `f` is concave on the convex hull of
`s`, then the eventual minimum of `f` on `convexHull 𝕜 s` lies in `s`. -/
theorem exists_le_of_mem_convexHull {t : Set E} (hf : ConcaveOn 𝕜 s f) (hts : t ⊆ s) (hx : x ∈ convexHull 𝕜 t) :
    ∃ y ∈ t, f y ≤ f x :=
  hf.dual.exists_ge_of_mem_convexHull hts hx

Похожие утверждения