theorem helperForTheorem_19_6_transport_liftedCone_sliceLemmas_toFinCoord {n m : ℕ} {C : Fin m.succ → Set (Fin n → ℝ)} (h_nonempty : ∀ (i : Fin m.succ), (C i).Nonempty) (h_closed : ∀ (i : Fin m.succ), IsClosed (C i)) (h_convex : ∀ (i : Fin m.succ), Convex ℝ (C i)) : have coords := fun (v : Fin (n + 1) → ℝ) => v; have first := fun (v : Fin (n + 1) → ℝ) => coords v 0; have tail := fun (v : Fin (n + 1) → ℝ) (i : Fin n) => coords v i.succ; have C0 := (convexHull ℝ) (⋃ (i : Fin m.succ), C i); have S0 := {v : Fin (n + 1) → ℝ | first v = 1 ∧ tail v ∈ C0}; have K0 := ↑(ConvexCone.hull ℝ S0); have S := fun (i : Fin m.succ) => {v : Fin (n + 1) → ℝ | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m.succ) => ↑(ConvexCone.hull ℝ (S i)); closure K0 = closure (∑ i : Fin m.succ, K i) ∧ closure C0 = {x : Fin n → ℝ | ∃ v ∈ closure K0, first v = 1 ∧ tail v = x} ∧ ∀ (v : Fin (n + 1) → ℝ), first v = 1 → (v ∈ ∑ i : Fin m.succ, closure (K i) ↔ ∃ (lam : Fin m.succ → ℝ), (∀ (i : Fin m.succ), 0 ≤ lam i) ∧ ∑ i : Fin m.succ, lam i = 1 ∧ tail v ∈ ∑ i : Fin m.succ, if lam i = 0 then (C i).recessionCone else lam i • C i)

Helper for Theorem 19.6: for a family indexed by Fin (m+1), the weighted-union formula for closure (convexHull (⋃ i, C i)) follows from the lifted-cone closure-sum identity.

theorem helperForTheorem_19_6_closure_convexHull_eq_weighted_union_core_noLineal {n m : ℕ} {C : Fin m.succ → Set (Fin n → ℝ)} (h_nonempty : ∀ (i : Fin m.succ), (C i).Nonempty) (h_closed : ∀ (i : Fin m.succ), IsClosed (C i)) (h_convex : ∀ (i : Fin m.succ), Convex ℝ (C i)) (hclosure_sum : have coords := fun (v : Fin (n + 1) → ℝ) => v; have first := fun (v : Fin (n + 1) → ℝ) => coords v 0; have tail := fun (v : Fin (n + 1) → ℝ) (i : Fin n) => coords v i.succ; have S := fun (i : Fin m.succ) => {v : Fin (n + 1) → ℝ | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m.succ) => ↑(ConvexCone.hull ℝ (S i)); closure (∑ i : Fin m.succ, K i) = ∑ i : Fin m.succ, closure (K i)) : closure ((convexHull ℝ) (⋃ (i : Fin m.succ), C i)) = ⋃ (lam : Fin m.succ → ℝ), ⋃ (_ : (∀ (i : Fin m.succ), 0 ≤ lam i) ∧ ∑ i : Fin m.succ, lam i = 1), ∑ i : Fin m.succ, if lam i = 0 then (C i).recessionCone else lam i • C i

Helper for Theorem 19.6: for a family indexed by Fin (m+1), the weighted-union formula for closure (convexHull (⋃ i, C i)) follows from the lifted-cone closure-sum identity.

theorem helperForTheorem_19_6_polyhedral_and_weightedUnion_core {n m : ℕ} {C : Fin m → Set (Fin n → ℝ)} (h_nonempty : ∀ (i : Fin m), (C i).Nonempty) (h_polyhedral : ∀ (i : Fin m), IsPolyhedralConvexSet n (C i)) : IsPolyhedralConvexSet n (closure ((convexHull ℝ) (⋃ (i : Fin m), C i))) ∧ closure ((convexHull ℝ) (⋃ (i : Fin m), C i)) = ⋃ (lam : Fin m → ℝ), ⋃ (_ : (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1), ∑ i : Fin m, if lam i = 0 then (C i).recessionCone else lam i • C i

Helper for Theorem 19.6: core closure/representation package for closure (convexHull (⋃ i, C i)) under polyhedral hypotheses.

theorem helperForTheorem_19_6_iUnionWeights_eq_weightedSumSubtype {n m : ℕ} {C : Fin m → Set (Fin n → ℝ)} : (⋃ (lam : Fin m → ℝ), ⋃ (_ : (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1), ∑ i : Fin m, if lam i = 0 then (C i).recessionCone else lam i • C i) = ⋃ (lam : { lam : Fin m → ℝ // (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 }), weightedSumSetWithRecession n m C ↑lam

Helper for Theorem 19.6: the explicit union over raw weight functions with simplex constraints is equivalent to the subtype-indexed union via weightedSumSetWithRecession.

theorem polyhedralConvexSet_closure_convexHull_iUnion_weightedSum (n m : ℕ) (C : Fin m → Set (Fin n → ℝ)) (C' : Set (Fin n → ℝ)) (hC' : C' = closure ((convexHull ℝ) (⋃ (i : Fin m), C i))) (h_nonempty : ∀ (i : Fin m), (C i).Nonempty) (h_polyhedral : ∀ (i : Fin m), IsPolyhedralConvexSet n (C i)) : IsPolyhedralConvexSet n C' ∧ C' = ⋃ (lam : { lam : Fin m → ℝ // (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 }), weightedSumSetWithRecession n m C ↑lam

Theorem 19.6: If C₁, …, Cₘ are non-empty polyhedral convex sets in ℝ^n and C = cl (conv (C₁ ∪ ··· ∪ Cₘ)), then C is polyhedral convex, and C is the union of weighted sums λ₁ C₁ + ··· + λₘ Cₘ over all choices of λ_i ≥ 0 with ∑ i, λ_i = 1, using 0^+ C_i in place of 0 • C_i when λ_i = 0.