English
If f is convex on t with s ⊆ t and f is bounded above on s, then f is bounded above on the convex hull of s.
Русский
Если f выпукла на t и s ⊆ t, и значения f на s ограничены сверху, то они также ограничены сверху на выпуклой оболочке s.
LaTeX
$$$ s \subseteq t \rightarrow \operatorname{ConvexOn}(\,\mathbb{K}, t, f) \rightarrow BddAbove\bigl(f'' s\bigr) \rightarrow BddAbove\bigl(f'' \operatorname{convexHull}(\,\mathbb{K}, s)\bigr)$$$
Lean4
theorem bddAbove_convexHull {s t : Set E} (hst : s ⊆ t) (hf : ConvexOn 𝕜 t f) :
BddAbove (f '' s) → BddAbove (f '' convexHull 𝕜 s) :=
by
rintro ⟨b, hb⟩
refine ⟨b, ?_⟩
rintro _ ⟨x, hx, rfl⟩
obtain ⟨y, hy, hxy⟩ := hf.exists_ge_of_mem_convexHull hst hx
exact hxy.trans <| hb <| mem_image_of_mem _ hy
