Existence of extreme points: a polyhedron has an extreme point iff it contains no line

Proved

LinearOptimization.polyhedron_extreme_point_existence

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

convexitygeometrylinear-programmingpolyhedra

(Theorem 2.6) Suppose that the polyhedron

P = \{x \in \mathbb{R}^n \mid a_i'x \ge b_i,\ i = 1, \dots, m\}

is nonempty. Then, the following are equivalent:

(a) The polyhedron $P$ has at least one extreme point.
(b) The polyhedron $P$ does not contain a line.
(c) There exist $n$ vectors out of the family $a_1, \dots, a_m$ , which are linearly independent.

Preamble

import Mathlib.Analysis.Convex.Extreme
import Mathlib.Data.List.TFAE
import Definitions.Def_Polyhedron
import Definitions.Def_ContainsLine


/-- **B&T Theorem 2.6 (p. 63).** Existence of extreme points of a nonempty
general-form polyhedron: extreme point exists ⟺ no line contained ⟺ some
`n` of the constraint vectors (= rows of `A`) are linearly independent. -/

Formal statement

theorem LinearOptimization.polyhedron_extreme_point_existence {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ)
    (hne : (polyhedron A b).Nonempty) :
    List.TFAE
      [ (Set.extremePoints ℝ (polyhedron A b)).Nonempty,
        ¬ ContainsLine (polyhedron A b),
        ∃ s : Finset (Fin m), s.card = n ∧
          LinearIndependent ℝ (fun i : s => A i.1) ] := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.6, p. 63

View graph