Attainment of the optimal cost in linear programming

Proved

LinearOptimization.lp_attains_or_unbounded

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

geometrylinear-programmingpolyhedra

(Corollary 2.3) Consider the linear programming problem of minimizing $c'x$ over a nonempty polyhedron.

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

(The book contrasts this with nonlinear problems: minimizing $1/x$ subject to $x \ge 1$ has finite optimal cost but no optimal solution.)

Preamble

import Definitions.Def_Polyhedron


/-- **B&T Corollary 2.3 (p. 67).** An LP over a nonempty polyhedron either
has optimal cost `−∞` or attains an optimal solution. -/

Formal statement

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

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Corollary 2.3, p. 67

View graph