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

Proved

LinearOptimization.lp_vertex_extreme_bfs_equiv

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

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

View graph

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

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