Characteristic cone is a convex cone; K is stable under translation by it
ProvedGrunbaum2003.characteristicCone_cone_basicsconvex-geometryrecession-conesource-faithful-child
For every natural dimension d and every set K in real d-dimensional space, the characteristic cone of K is a convex set containing the zero vector, and K translated by any element of the characteristic cone stays inside K.
Preamble
import Definitions.Def_auto_GRUM02ER_1c2100_Grunbaum2003_RecessionDefinitions set_option autoImplicit false open scoped Pointwise
Formal statement
namespace Grunbaum2003
theorem characteristicCone_cone_basics {d : ℕ}
(K : Set (Fin d → ℝ)) :
Convex ℝ (characteristicCone K) ∧ (0 : Fin d → ℝ) ∈ characteristicCone K ∧
K + characteristicCone K ⊆ K := 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.