An unbounded primal has an infeasible dual

Proved

LinearOptimization.lp_unbounded_dual_infeasible

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

dualitylinear-programmingunboundedness

(Corollary 4.1)

(a) If the optimal cost in the primal is $-\infty$ , then the dual problem must be infeasible.
(b) If the optimal cost in the dual is $+\infty$ , then the primal problem must be infeasible.

Preamble

import Definitions.Def_LinearOptimization_DualLP


/-- **Bertsimas & Tsitsiklis, Corollary 4.1 (p. 147).** (a) A primal with optimal cost `−∞`
has an infeasible dual; (b) a dual with optimal cost `+∞` has an
infeasible primal. -/

Formal statement

theorem LinearOptimization.lp_unbounded_dual_infeasible {m n : ℕ} (P : GeneralFormLP m n) :
    (lpValue P.c (generalFeasibleSet P) = ⊥ →
      generalFeasibleSet (dualLP P) = ∅) ∧
    (lpDualValue P.b (generalFeasibleSet (dualLP P)) = ⊤ →
      generalFeasibleSet P = ∅) := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Corollary 4.1, p. 147

View graph