convex_strict_epigraph — Mathlib

English

Convexon a convex subset implies the epigraph is convex under zero-one scaling assumptions.

Русский

Выпуклость множества переходит в выпуклость эпиграфа при нулево-единичных предположениях.

LaTeX

$$$\text{ZeroOneClass 𝕜} \Rightarrow (\text{ConvexOn } s f) \Rightarrow (\text{Convex } \{(x,t)\mid x\in s, t>f(x)\})$$$

Lean4

theorem convex_strict_epigraph [ZeroLEOneClass 𝕜] (hf : ConvexOn 𝕜 s f) :
    Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} :=
  convex_iff_openSegment_subset.mpr fun p hp q hq => hf.openSegment_subset_strict_epigraph p q hp ⟨hq.1, hq.2.le⟩

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