Convexity of polyhedra
ProvedLinearOptimization.polyhedron_convexconvexitylinear-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