Theorem 4.4.1 — vertices are exactly the basic feasible solutions

Let $A$ be a real $m\times n$ matrix of rank $m$ with $n\ge m$ and $n\ge 1$, let $b\in\mathbb{R}^m$, and let

be the set of feasible solutions of the linear program in equational form. For a point $v\in P$ the following are equivalent:

1. $v$ is a vertex of $P$: there is a nonzero $c\in\mathbb{R}^n$ with $c^{T}v>c^{T}y$ for all $y\in P\setminus\{v\}$;
2. $v$ is a basic feasible solution of the linear program.

The theorem identifies the algebraic notion used by the simplex method with the geometric "corners" of the feasible polyhedron.

Formalization Note The standing assumption of §4.2 (p. 44), $n\ge m$ and $\operatorname{rank}A=m$, is a hypothesis. The hypothesis $n\ge 1$ is added: for $n=0$ there is no nonzero $c\in\mathbb{R}^0$, so the unique feasible point $0$ is basic (with $B=\emptyset$) but not a vertex in the book's sense, and the equivalence fails; the book tacitly works with $n\ge 1$. "Vertex" is the book's unique-maximizer definition, not Mathlib's extreme points.