convexOn_of_convex_epigraph — Mathlib

English

If f is convex on s, then the epigraph of f over s is a convex set.

Русский

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

LaTeX

$$$ConvexOn\ 𝕜\ s\ f \Rightarrow Convex\ 𝕜\ {p : E \times β \mid p.1 \in s \wedge p.2 \ge f(p.1)}$$$

Lean4

theorem convexOn_of_convex_epigraph (h : Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}) : ConvexOn 𝕜 s f :=
  ⟨fun x hx y hy a b ha hb hab => (@h (x, f x) ⟨hx, le_rfl⟩ (y, f y) ⟨hy, le_rfl⟩ a b ha hb hab).1,
    fun x hx y hy a b ha hb hab => (@h (x, f x) ⟨hx, le_rfl⟩ (y, f y) ⟨hy, le_rfl⟩ a b ha hb hab).2⟩

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