Some optimal solution is an extreme point

Proved

LinearOptimization.lp_optimal_extreme_point

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

convexitygeometrylinear-programmingpolyhedra

(Theorem 2.7) Consider the linear programming problem of minimizing $c'x$ over a polyhedron $P$ . Suppose that $P$ has at least one extreme point and that there exists an optimal solution.

Then, there exists an optimal solution which is an extreme point of $P$ .

Preamble

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


/-- **B&T Theorem 2.7 (p. 65).** If the feasible polyhedron has an extreme
point and the LP has an optimal solution, then some extreme point is
optimal. -/

Formal statement

theorem LinearOptimization.lp_optimal_extreme_point {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) (c : Fin n → ℝ)
    (hext : (Set.extremePoints ℝ (polyhedron A b)).Nonempty)
    (hopt : ∃ x, IsLpOptimal c (polyhedron A b) x) :
    ∃ 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.7, p. 65

View graph