bddBelow_convexHull — Mathlib

English

Let s ⊆ t and f be concave on t. If f is bounded below on s, then f is bounded below on the convex hull of s.

Русский

Пусть s ⊆ t и f вогнута на t. Если f ограничена снизу на s, то она ограничена снизу на выпуклой оболочке s.

LaTeX

$$$ s \subseteq t \rightarrow \operatorname{ConcaveOn}(\,\mathbb{K}, t, f) \rightarrow BddBelow\bigl(f'' s\bigr) \rightarrow BddBelow\bigl(f'' \operatorname{convexHull}(\,\mathbb{K}, s)\bigr)$$$

Lean4

theorem bddBelow_convexHull {s t : Set E} (hst : s ⊆ t) (hf : ConcaveOn 𝕜 t f) :
    BddBelow (f '' s) → BddBelow (f '' convexHull 𝕜 s) :=
  hf.dual.bddAbove_convexHull hst

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