ConvexOn — Mathlib

English

The extreme points of the convex hull of A are contained in A.

Русский

Крайние точки выпуклой оболочки A содержатся в A.

LaTeX

$$$\operatorname{extremePoints}_{𝕜}(\operatorname{convexHull}_{𝕜} A) \subseteq A$$$

Lean4

/-- Convexity of functions -/
def ConvexOn : Prop :=
  Convex 𝕜 s ∧
    ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

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