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⟩