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

Proved

LinearOptimization.polyhedron_extreme_point_existence

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

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

Read-back

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

Let $A$ be a real $m \times n$ matrix and $b \in \mathbb{R}^m$ , and assume the polyhedron $P = \{x \in \mathbb{R}^n \mid Ax \ge b \text{ componentwise}\}$ is nonempty. The theorem asserts that the following three are pairwise equivalent: (1) $P$ has at least one extreme point in Mathlib's sense (a point of $P$ that never lies strictly inside an open segment between two points of $P$ unless both endpoints equal it); (2) $P$ does not contain a full affine line (there are no $x \in P$ and $d \ne 0$ with $x + \lambda d \in P$ for all $\lambda \in \mathbb{R}$ ); (3) there exists a finite set $s$ of row indices with exactly $n$ elements such that the corresponding rows $(A_i)_{i \in s}$ of $A$ are linearly independent — equivalently, $A$ has $n$ linearly independent rows (which requires $m \ge n$ ; when $n = 0$ the empty set works and (3) is automatically true). Note that condition (3) refers only to the matrix $A$ , not to $b$ or to which constraints are active anywhere.

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