Line-free closed convex sets have an extreme point
ProvedGrunbaum2003.closed_convex_line_free_extremePoint_existsconvex-geometryextreme-pointsline-freesource-faithful-child
For every natural dimension d, every nonempty closed convex line-free set K in real d-dimensional space has an extreme point.
Preamble
import Definitions.Def_auto_GRUM02ER_1c2100_Grunbaum2003_RecessionDefinitions set_option autoImplicit false open scoped Pointwise
Formal statement
namespace Grunbaum2003
theorem closed_convex_line_free_extremePoint_exists {d : ℕ}
(K : Set (Fin d → ℝ)) (hne : K.Nonempty) (hline : IsLineFree K)
(hclosed : IsClosed K) (hconvex : Convex ℝ K) :
(K.extremePoints ℝ).Nonempty := 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.