convexOn_iff_convex_epigraph

Mathlib.Analysis.Convex.Function

URI: https://scilib.ai/kg/mathlib#convexOn_iff_convex_epigraph

← MathLib Explorer

English

ConvexOn 𝕜 s f if and only if the epigraph of f over s is convex.

Русский

ConvexOn 𝕜 s f эквивалентна выпуклости эпиграфа над s.

LaTeX

$$$ConvexOn\ 𝕜\ s\ f \iff Convex\ 𝕜\ {p : E \times β | p.1 \in s ∧ f(p.1) \le p.2}$$$

Lean4

theorem convexOn_iff_convex_epigraph : ConvexOn 𝕜 s f ↔ Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
  ⟨ConvexOn.convex_epigraph, convexOn_of_convex_epigraph⟩

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

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

Разделы

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

Аффилиация

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