convexOn — Mathlib

English

If a function is strictly convex on a set, then it is convex on that set (alternative form).

Русский

Если функция строго выпукла на множестве, то она выпукла на нём.

LaTeX

$$$StrictConvexOn\ 𝕜\ s\ f \rightarrow ConvexOn\ 𝕜\ s\ f$$$

Lean4

theorem convexOn {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) : ConvexOn 𝕜 s f :=
  convexOn_iff_pairwise_pos.mpr ⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab => (hf.2 hx hy hxy ha hb hab).le⟩

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