Extreme-point optimality: optimal cost $-\infty$ or an optimal extreme point

Proved

LinearOptimization.lp_extreme_point_optimality

by Shuze Chen · Aug 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexitygeometrylinear-programmingpolyhedra

(Theorem 2.8, GOAL) Consider the linear programming problem of minimizing $c'x$ over a polyhedron $P$ . Suppose that $P$ has at least one extreme point.

Then, either the optimal cost is equal to $-\infty$ , or there exists an extreme point which is optimal.

Preamble

import Mathlib.Analysis.Convex.Extreme
import Definitions.Def_Polyhedron


/-- **B&T Theorem 2.8 (p. 66).** Over a polyhedron with at least one extreme
point, either the optimal cost is `−∞` or some extreme point is optimal. -/

Formal statement

theorem LinearOptimization.lp_extreme_point_optimality {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) (c : Fin n → ℝ)
    (hext : (Set.extremePoints ℝ (polyhedron A b)).Nonempty) :
    lpValue c (polyhedron A b) = ⊥ ∨
      ∃ x ∈ Set.extremePoints ℝ (polyhedron A b),
        IsLpOptimal c (polyhedron A b) x := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.8, p. 66

View graph

Extreme-point optimality: optimal cost −∞-\infty−∞ or an optimal extreme point

Extreme-point optimality: optimal cost $-\infty$ or an optimal extreme point