convex_strict_hypograph

Mathlib.Analysis.Convex.Function

URI: https://scilib.ai/kg/mathlib#ConcaveOn.convex_strict_hypograph

← MathLib Explorer

English

If f is concave, the hypograph is convex under strict monotonicity.

Русский

Если f вогнутая, гипограф выпукл при строгой монотонности.

LaTeX

$$$\text{ConcaveOn } f \Rightarrow \text{hypograph is convex}$$$

Lean4

theorem convex_strict_hypograph [ZeroLEOneClass 𝕜] (hf : ConcaveOn 𝕜 s f) :
    Convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 < f p.1} :=
  hf.dual.convex_strict_epigraph

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru