convex_gt — Mathlib

English

If f is strictly concave on s, then the epigraph of f over s has convexity properties reflected in related sets.

Русский

Если f строго вогнутая на s, то эпиграф f над s имеет выпуклость в сопряжённых множествах.

LaTeX

$$$\text{See dual statements: }\text{StrictConcaveOn} \Rightarrow \text{ConvexOn}$$$

Lean4

theorem convex_gt (hf : StrictConcaveOn 𝕜 s f) (r : β) : Convex 𝕜 ({x ∈ s | r < f x}) :=
  hf.dual.convex_lt r

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