Convex hull of a compact set is compact in finite dimensions
ProvedGrunbaum2003.isCompact_convexHull_of_compactcompactnessconvex-geometrymathlib-gapsource-faithful-child
For every natural dimension d, the convex hull of a compact set in real d-dimensional space is compact.
Preamble
import Definitions.Def_auto_GRUM02ER_1c2100_Grunbaum2003_RecessionDefinitions set_option autoImplicit false open scoped Pointwise
Formal statement
namespace Grunbaum2003
theorem isCompact_convexHull_of_compact {d : ℕ}
(s : Set (Fin d → ℝ)) (h : IsCompact s) :
IsCompact (convexHull ℝ s) := by sorry
end Grunbaum2003
Source
Branko Grünbaum, Convex Polytopes, second edition (2003), §2.5, Theorem 6 (2.5.6), printed p.25 / source.pdf p.43; characteristic cone and line-free sets: printed p.24 / PDF42; extreme points: §2.4, printed p.17 / PDF35.