Convexity of polyhedra

Proved

LinearOptimization.polyhedron_convex

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

convexitylinear-programmingpolyhedra

(Theorem 2.1, part (b) formalized) Every polyhedron is a convex set.

The book's full statement:

(a) The intersection of convex sets is convex.
(b) Every polyhedron is a convex set.
(c) A convex combination of a finite number of elements of a convex set also belongs to that set.
(d) The convex hull of a finite number of vectors is a convex set.

Encoding: Parts (a), (c), (d) are Mathlib (Convex.inter/convex_iInter, Convex.sum_mem, convex_convexHull); the item is part (b) for the polyhedron Def of this mission.

Preamble

import Mathlib.Analysis.Convex.Basic
import Definitions.Def_Polyhedron


/-- **B&T Theorem 2.1(b) (p. 44).** Every polyhedron `{x | Ax ≥ b}` is a
convex set. -/

Formal statement

theorem LinearOptimization.polyhedron_convex {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) : Convex ℝ (polyhedron A b) := by sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.1, p. 44

Read-back

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

For all natural numbers $m, n$ , every real $m \times n$ matrix $A$ , and every $b \in \mathbb{R}^m$ , the set $\{x \in \mathbb{R}^n \mid b \le Ax \text{ componentwise}\}$ (the bundle's " $\ge$ "-form polyhedron) is convex over $\mathbb{R}$ in the standard sense: for any two points $x, y$ of the set and any $s, t \ge 0$ with $s + t = 1$ , the combination $s\,x + t\,y$ is also in the set. This includes the degenerate cases $m = 0$ (the set is all of $\mathbb{R}^n$ ), $n = 0$ , and an empty polyhedron (convex vacuously). There are no further hypotheses.

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