theorem Set.pos_smul_isCone {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) : IsCone (Ioi 0 • C)

Helper for Proposition 6.2: the set of strictly positive multiples of a set is itself a cone.

theorem Set.smul_subset_of_isCone {E : Type u} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : IsCone K) {a : ℝ} (ha : 0 < a) : a • K ⊆ K

Helper for Proposition 6.2: a cone is stable under any fixed strictly positive scalar.

theorem Set.conicalHull_eq_pos_smul {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) : C.conicalHull = Ioi 0 • C

Proposition 6.2 (1): textbook clause (i). The conical hull cone C is exactly the set of strictly positive real multiples of points of C.

theorem Set.conicalHull_eq_convexConeHull_of_convex {E : Type u} [AddCommGroup E] [Module ℝ E] {C : Set E} (hC : Convex ℝ C) : C.conicalHull = ↑(ConvexCone.hull ℝ C)

Helper for Proposition 6.2: on a convex set, the source conical hull agrees with the bundled convex-cone hull.

theorem Set.convexHull_isCone_of_isCone {E : Type u} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : IsCone K) : IsCone ((convexHull ℝ) K)

Helper for Proposition 6.2: taking the convex hull of a cone preserves the cone property.

theorem Set.conicalHull_convexHull_eq_convexHull_conicalHull {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) : ((convexHull ℝ) C).conicalHull = (convexHull ℝ) C.conicalHull

Proposition 6.2 (2): textbook clause (iii). Taking the conical hull after the convex hull agrees with taking the convex hull after the conical hull.

theorem Set.conicalHull_convexHull_eq_convexConeHull {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) : ((convexHull ℝ) C).conicalHull = ↑(ConvexCone.hull ℝ C)

Bridge to the canonical owner: cone (convexHull ℝ C) is the underlying set of the convex cone hull of C.

theorem Set.closure_isCone_of_isCone {E : Type u} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [ContinuousConstSMul ℝ E] {K : Set E} (hK : IsCone K) : IsCone (closure K)

Helper for Proposition 6.2: the closure of a cone is still a cone.

theorem Set.closure_conicalHull_eq_closedConicalHull {E : Type u} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [ContinuousConstSMul ℝ E] (C : Set E) : closure C.conicalHull = C.closedConicalHull

Proposition 6.2 (7): textbook clause (ii). The closure of cone C is its closed conical hull.

theorem Set.closedConicalHull_convexHull_eq_closure_convexConeHull {E : Type u} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [ContinuousAdd E] [ContinuousConstSMul ℝ E] (C : Set E) : ((convexHull ℝ) C).closedConicalHull = ↑(ConvexCone.hull ℝ C).closure

Proposition 6.2 (8): textbook clause (iv). The closed conical hull of the convex hull of C agrees with the closure of the canonical convex cone hull of C.