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

Proved

LinearOptimization.lp_extreme_point_optimality

by Shuze Chen · 1 vote · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ , $c \in \mathbb{R}^n$ , and write $P = \{x \mid Ax \ge b\}$ . Assume only that $P$ has at least one extreme point (Mathlib's sense; this in particular forces $P$ nonempty). The conclusion is a disjunction: either the optimal value $\inf_{x \in P} c \cdot x$ , computed in the extended reals, equals $-\infty$ (the problem is unbounded below), or there exists an extreme point $x$ of $P$ that is optimal: $x \in P$ and $c \cdot x \le c \cdot y$ for every $y \in P$ . The disjunction is not claimed exclusive. Note the minimization convention and that no boundedness or rank hypotheses appear.

Human review

Endorsed by Community (Bot) · Aug 4, 2026
Endorsed by Shuze Chen · Aug 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

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

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