Theorem 10.4 — Separation Theorem for polyhedra

Open

VanderbeiLP.StrictComp.separation_polyhedra

by mikedeng1 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-analysisp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1polyhedraseparation

Let $P$ and $\tilde P$ be two polyhedra in $\mathbb{R}^n$ , i.e. sets of the form $\{x : Ax \le b\}$ and $\{x : \tilde A x \le \tilde b\}$ . If $P$ and $\tilde P$ are both nonempty and disjoint, then there exist halfspaces $H$ and $\tilde H$ with

P \subseteq H, \qquad \tilde P \subseteq \tilde H, \qquad H \cap \tilde H = \emptyset.

Here a halfspace is a set $\{x : a^T x \le \beta\}$ with $a \ne 0$ , so the two separating sets are genuine halfspaces with nonzero (and necessarily opposite-pointing) normals, not all of $\mathbb{R}^n$ or the empty set.

The theorem is the polyhedral case of the separating hyperplane theorem, obtained without any topology.

Formalization Note The book's " $P \subset H$ " is inclusion (not necessarily proper). Both nonemptiness hypotheses are kept: they are what forces the normals to be nonzero.

Preamble

import Mathlib
import Definitions.Def_VanderbeiLP_StrictComp_Polyhedron

Formal statement

namespace VanderbeiLP.StrictComp

/-- **Vanderbei, Theorem 10.4 (p. 145), Separation Theorem for polyhedra.** Two disjoint
nonempty polyhedra `P`, `P̃` of `ℝⁿ` lie in disjoint halfspaces `H ⊇ P`, `H̃ ⊇ P̃`
(halfspaces in the sense of (10.3): nonzero normal). -/
theorem separation_polyhedra {n : ℕ} (P Ptil : Set (Fin n → ℝ))
    (hP : IsPolyhedron P) (hPtil : IsPolyhedron Ptil)
    (hPne : P.Nonempty) (hPtilne : Ptil.Nonempty) (hdisj : Disjoint P Ptil) :
    ∃ H Htil : Set (Fin n → ℝ), IsHalfspace H ∧ IsHalfspace Htil ∧ Disjoint H Htil ∧
      P ⊆ H ∧ Ptil ⊆ Htil := by sorry

end VanderbeiLP.StrictComp

Source

Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer 2014, p. 145, Theorem 10.4 (PDF p. 158); halfspace Eq. (10.3), p. 144

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph