concaveOn_of_convex_hypograph — Mathlib

English

If the hypograph of f over s is convex, then f is concave on s.

Русский

Если гипопиграф функции над s выпукл, то функция выпукла на s абсолютизированно? (множество)

LaTeX

$$$ConcaveOn\ 𝕜\ s\ f \leftarrow Convex\ 𝕜\ {p : E \times β \mid p.1 \in s \wedge p.2 \le f(p.1)}$$$

Lean4

theorem concaveOn_of_convex_hypograph (h : Convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}) : ConcaveOn 𝕜 s f :=
  convexOn_of_convex_epigraph (β := βᵒᵈ) h

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