Vertex $=$ extreme point $=$ basic feasible solution

Proved

LinearOptimization.lp_vertex_extreme_bfs_equiv

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

convexitygeometrylinear-programmingpolyhedra

(Theorem 2.3, GOAL) Let $P$ be a nonempty polyhedron and let $x^* \in P$ . Then, the following are equivalent:

(a) $x^*$ is a vertex;
(b) $x^*$ is an extreme point;
(c) $x^*$ is a basic feasible solution.

(Stated for a fixed constraint representation of $P$ ; the book proves it, without loss of generality, for representations by constraints of the form $a_i'x \ge b_i$ and $a_i'x = b_i$ .)

Preamble

import Mathlib.Analysis.Convex.Extreme
import Mathlib.Data.List.TFAE
import Definitions.Def_Vertex
import Definitions.Def_BasicSolution


/-- **B&T Theorem 2.3 (p. 50).** For a nonempty polyhedron presented by the
constraint family `C` and `x* ∈ P`: vertex ⟺ extreme point ⟺ basic feasible
solution. -/

Formal statement

theorem LinearOptimization.lp_vertex_extreme_bfs_equiv {ι : Type} [Fintype ι] {n : ℕ}
    (C : ι → LinearConstraint n) (x' : Fin n → ℝ)
    (hne : (constraintSet C).Nonempty) (hx : x' ∈ constraintSet C) :
    List.TFAE
      [ IsVertex (constraintSet C) x',
        x' ∈ Set.extremePoints ℝ (constraintSet C),
        IsBasicFeasibleSolution C x' ] := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.3, p. 50

Read-back

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

Let $\iota$ be a finite type and $C : \iota \to$ linear constraints on $\mathbb{R}^n$ , with feasible set $F = \{x \mid \text{every } C_i \text{ satisfied at } x\}$ . Assume $F$ is nonempty and $x' \in F$ . The theorem asserts that the following three are pairwise equivalent: (1) $x'$ is a vertex of $F$ in the bundle's sense: there exists $c \in \mathbb{R}^n$ with $c \cdot x' < c \cdot y$ (strictly) for every $y \in F$ , $y \ne x'$ ; (2) $x'$ is an extreme point of $F$ in Mathlib's sense: $x' \in F$ and whenever $x'$ lies strictly between two points of $F$ — i.e. $x' = t x_1 + (1-t) x_2$ with $x_1, x_2 \in F$ and $0 < t < 1$ — one has $x_1 = x'$ and $x_2 = x'$ ; (3) $x'$ is a basic feasible solution: every " $=$ "-tagged constraint is active at $x'$ , and some $n$ -element finite index set $s$ has all its constraints active at $x'$ with $(a_i)_{i \in s}$ linearly independent. (For (3) with $n > \#\iota$ no such $s$ can exist.)

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

Vertex === extreme point === basic feasible solution

Vertex $=$ extreme point $=$ basic feasible solution