theorem helperForTheorem_19_7_closure_convexConeGenerated_eq_closure_hull {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) : closure (convexConeGenerated n C) = closure ↑(ConvexCone.hull ℝ C)

Helper for Theorem 19.7: for nonempty C, adjoining 0 to the cone hull does not change the closure.

theorem helperForTheorem_19_7_recessionCone_transport_eq {n : ℕ} {C : Set (Fin n → ℝ)} : have e := EuclideanSpace.equiv (Fin n) ℝ; ⇑e '' (⇑e.symm '' C).recessionCone = C.recessionCone

Helper for Theorem 19.7: the Euclidean-coordinate transport of the recession cone term equals the ambient-space recession cone.

theorem helperForTheorem_19_7_iUnion_pos_subtype_rewrite {n : ℕ} {C : Set (Fin n → ℝ)} : ⋃ (t : ℝ), ⋃ (_ : 0 < t), t • C = ⋃ (lam : { lam : ℝ // 0 < lam }), ↑lam • C

Helper for Theorem 19.7: rewriting the positive-scaling union from nested existential indices to a subtype index.

theorem helperForTheorem_19_7_originMem_directions_subset_carrier {n : ℕ} {C S₀ S₁ : Set (Fin n → ℝ)} (hCeq : C = mixedConvexHull S₀ S₁) (hC0 : 0 ∈ C) : S₁ ⊆ C

Helper for Theorem 19.7: if 0 ∈ C = mixedConvexHull S₀ S₁, then every direction generator belongs to C.

theorem helperForTheorem_19_7_recessionCone_subset_of_origin_mem {n : ℕ} {C : Set (Fin n → ℝ)} (hC0 : 0 ∈ C) : C.recessionCone ⊆ C

Helper for Theorem 19.7: if the origin belongs to C, then every recession direction of C lies in C.

theorem helperForTheorem_19_7_originMem_convexConeGenerated_eq_finiteCone {n : ℕ} {C S₀ S₁ : Set (Fin n → ℝ)} (hCeq : C = mixedConvexHull S₀ S₁) (hS₀fin : S₀.Finite) (hS₁fin : S₁.Finite) (hC0 : 0 ∈ C) : convexConeGenerated n C = cone n (S₀ ∪ S₁)

Helper for Theorem 19.7: with finite mixed-hull data and 0 ∈ C, the generated cone of C coincides with the finite cone generated by points and directions.

theorem polyhedralConvexCone_closure_convexConeGenerated (n : ℕ) (C : Set (Fin n → ℝ)) : C.Nonempty → IsPolyhedralConvexSet n C → IsPolyhedralConvexSet n (closure (convexConeGenerated n C)) ∧ IsConeSet n (closure (convexConeGenerated n C)) ∧ closure (convexConeGenerated n C) = (⋃ (lam : { lam : ℝ // 0 < lam }), ↑lam • C) ∪ C.recessionCone

Theorem 19.7: Let C be a non-empty polyhedral convex set, and let K be the closure of the convex cone generated by C. Then K is a polyhedral convex cone, and K = ⋃ {λ C | λ > 0 or λ = 0^+}.

theorem helperForCorollary_19_7_1_finitelyGenerated_of_polyhedral {n : ℕ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolyhedralConvexSet n C) : IsFinitelyGeneratedConvexSet n C

Helper for Corollary 19.7.1: a polyhedral convex set is finitely generated.

theorem polyhedral_convexConeGenerated_of_origin_mem (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → 0 ∈ C → IsPolyhedralConvexSet n (convexConeGenerated n C)

Corollary 19.7.1: If C is a polyhedral convex set containing the origin, the convex cone generated by C is polyhedral.