theorem helperForTheorem_19_6_weightedSumSetWithRecession_eq_finsetSumIf {n m : ℕ} {C : Fin m → Set (Fin n → ℝ)} {lam : Fin m → ℝ} : weightedSumSetWithRecession n m C lam = ∑ i : Fin m, if lam i = 0 then (C i).recessionCone else lam i • C i

Helper for Theorem 19.6: weightedSumSetWithRecession is exactly the finite Minkowski sum of the branch sets if λᵢ = 0 then 0⁺Cᵢ else λᵢ • Cᵢ.

theorem helperForTheorem_19_6_polyhedral_component_if_zero_or_scaled {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)) (lam : Fin m → ℝ) (i : Fin m) : IsPolyhedralConvexSet n (if lam i = 0 then (C i).recessionCone else lam i • C i)

Helper for Theorem 19.6: for each index i, the branch set if λᵢ = 0 then 0⁺Cᵢ else λᵢ • Cᵢ is polyhedral.

theorem helperForTheorem_19_6_polyhedral_finset_sum {n m : ℕ} {S : Fin m → Set (Fin n → ℝ)} (hS_poly : ∀ (i : Fin m), IsPolyhedralConvexSet n (S i)) : IsPolyhedralConvexSet n (∑ i : Fin m, S i)

Helper for Theorem 19.6: finite Minkowski sums of polyhedral convex sets are polyhedral.

theorem helperForTheorem_19_6_closed_convex_of_polyhedral_family {n m : ℕ} {C : Fin m → Set (Fin n → ℝ)} (h_polyhedral : ∀ (i : Fin m), IsPolyhedralConvexSet n (C i)) : (∀ (i : Fin m), IsClosed (C i)) ∧ ∀ (i : Fin m), Convex ℝ (C i)

Helper for Theorem 19.6: polyhedral family members are closed and convex.

theorem helperForTheorem_19_6_closure_sum_liftedCones_eq_sum_closure_liftedCones_polyhedral {n m : ℕ} {K : Fin m → Set (Fin (n + 1) → ℝ)} (hK_poly : ∀ (i : Fin m), IsPolyhedralConvexSet (n + 1) (closure (K i))) : closure (∑ i : Fin m, K i) = ∑ i : Fin m, closure (K i)

Helper for Theorem 19.6: if each closure (K i) is polyhedral, then closure (∑ i, K i) = ∑ i, closure (K i).

theorem helperForTheorem_19_6_polyhedral_empty_set {n : ℕ} : IsPolyhedralConvexSet n ∅

Helper for Theorem 19.6: the empty set in ℝ^n is polyhedral.

theorem helperForTheorem_19_6_polyhedral_emptyClosureConvexHull_fin0 {n : ℕ} {C : Fin 0 → Set (Fin n → ℝ)} : IsPolyhedralConvexSet n (closure ((convexHull ℝ) (⋃ (i : Fin 0), C i)))

Helper for Theorem 19.6: when the index set is Fin 0, the closed convex hull of the union is polyhedral.

theorem helperForTheorem_19_6_nonempty_transport_toEuclidean {n : ℕ} {C : Set (Fin n → ℝ)} (hC_nonempty : C.Nonempty) : (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C).Nonempty

Helper for Theorem 19.6: transporting nonemptiness from Fin n → ℝ to EuclideanSpace ℝ (Fin n) via EuclideanSpace.equiv.symm.

theorem helperForTheorem_19_6_closed_transport_toEuclidean {n : ℕ} {C : Set (Fin n → ℝ)} (hC_closed : IsClosed C) : IsClosed (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C)

Helper for Theorem 19.6: transporting closedness from Fin n → ℝ to EuclideanSpace ℝ (Fin n) via EuclideanSpace.equiv.symm.

theorem helperForTheorem_19_6_convex_transport_toEuclidean {n : ℕ} {C : Set (Fin n → ℝ)} (hC_convex : Convex ℝ C) : Convex ℝ (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C)

Helper for Theorem 19.6: transporting convexity from Fin n → ℝ to EuclideanSpace ℝ (Fin n) via EuclideanSpace.equiv.symm.

theorem helperForTheorem_19_6_finEuclidean_firstTail_bridge {n : ℕ} : have eNp1 := ⇑(EuclideanSpace.equiv (Fin (n + 1)) ℝ).symm; have coordsE := ⇑(EuclideanSpace.equiv (Fin (n + 1)) ℝ); have firstE := fun (v : EuclideanSpace ℝ (Fin (n + 1))) => coordsE v 0; have tailE := fun (v : EuclideanSpace ℝ (Fin (n + 1))) (i : Fin n) => coordsE v i.succ; (∀ (v : Fin (n + 1) → ℝ), firstE (eNp1 v) = v 0) ∧ ∀ (v : Fin (n + 1) → ℝ), tailE (eNp1 v) = fun (i : Fin n) => v i.succ

Helper for Theorem 19.6: explicit coordinate identities between the Fin model and EuclideanSpace via EuclideanSpace.equiv.

theorem helperForTheorem_19_6_nonempty_liftedSlice {n : ℕ} {C : Set (Fin n → ℝ)} (hC_nonempty : C.Nonempty) : {v : Fin (n + 1) → ℝ | v 0 = 1 ∧ (fun (j : Fin n) => v j.succ) ∈ C}.Nonempty

Helper for Theorem 19.6: the lifted slice {v | v₀ = 1, tail v ∈ C} is nonempty whenever C is nonempty.

theorem helperForTheorem_19_6_polyhedral_liftedSlice {n : ℕ} {C : Set (Fin n → ℝ)} (hC_polyhedral : IsPolyhedralConvexSet n C) : IsPolyhedralConvexSet (n + 1) {v : Fin (n + 1) → ℝ | v 0 = 1 ∧ (fun (j : Fin n) => v j.succ) ∈ C}

Helper for Theorem 19.6: polyhedrality of a base set C implies polyhedrality of the lifted slice {v | v₀ = 1, tail v ∈ C}.

theorem helperForTheorem_19_6_points_subset_mixedConvexHull {d : ℕ} {S₀ S₁ : Set (Fin d → ℝ)} : S₀ ⊆ mixedConvexHull S₀ S₁

Helper for Theorem 19.6: every point-generator belongs to its mixed convex hull.

theorem helperForTheorem_19_6_directions_subset_recessionCone_mixedConvexHull {d : ℕ} {S₀ S₁ : Set (Fin d → ℝ)} : S₁ ⊆ (mixedConvexHull S₀ S₁).recessionCone

Helper for Theorem 19.6: every direction-generator is a recession direction of the mixed convex hull generated by the same data.

theorem helperForTheorem_19_6_recessionDirection_mem_closure_convexConeHull_of_nonempty {d : ℕ} {C : Set (Fin d → ℝ)} (hC_nonempty : C.Nonempty) {dir : Fin d → ℝ} (hdir : dir ∈ C.recessionCone) : dir ∈ closure ↑(ConvexCone.hull ℝ C)

Helper for Theorem 19.6: every recession direction of a nonempty set lies in the closure of the convex cone generated by that set.

theorem helperForTheorem_19_6_closure_convexConeHull_eq_cone_of_finiteMixedData {d : ℕ} {S₀ S₁ : Set (Fin d → ℝ)} (hS₀fin : S₀.Finite) (hS₁fin : S₁.Finite) (hS₀ne : S₀.Nonempty) : closure ↑(ConvexCone.hull ℝ (mixedConvexHull S₀ S₁)) = cone d (S₀ ∪ S₁)

Helper for Theorem 19.6: closure of the convex cone generated by a finite mixed hull equals the cone generated by the union of finite point and direction generators.

theorem helperForTheorem_19_6_polyhedral_closure_convexConeHull_of_polyhedral {d : ℕ} {S : Set (Fin d → ℝ)} (hS_nonempty : S.Nonempty) (hS_polyhedral : IsPolyhedralConvexSet d S) : IsPolyhedralConvexSet d (closure ↑(ConvexCone.hull ℝ S))

Helper for Theorem 19.6: closure of the convex cone generated by a nonempty polyhedral set is polyhedral.

theorem helperForTheorem_19_6_convexHull_iUnion_image_linearEquiv {n m : ℕ} {C : Fin m.succ → Set (Fin n → ℝ)} : have eN := (EuclideanSpace.equiv (Fin n) ℝ).symm; have CE := fun (i : Fin m.succ) => ⇑eN '' C i; ⇑eN '' (convexHull ℝ) (⋃ (i : Fin m.succ), C i) = (convexHull ℝ) (⋃ (i : Fin m.succ), CE i)

Helper for Theorem 19.6: transporting convexHull of a finite union through the Euclidean coordinate equivalence.

theorem helperForTheorem_19_6_image_finsetSum_addEquiv {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Fintype ι] (e : α ≃+ β) (A : ι → Set α) : ⇑e '' ∑ i : ι, A i = ∑ i : ι, ⇑e '' A i

Helper for Theorem 19.6: additive equivalences commute with finite Minkowski sums.

theorem helperForTheorem_19_6_preimage_finsetSum_addEquiv {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Fintype ι] (e : α ≃+ β) (A : ι → Set β) : ⇑e ⁻¹' ∑ i : ι, A i = ∑ i : ι, ⇑e ⁻¹' A i

Helper for Theorem 19.6: additive equivalences commute with finite Minkowski sums under preimage.

theorem helperForTheorem_19_6_image_weightedUnion_linearEquiv {n m : ℕ} {C : Fin m.succ → Set (Fin n → ℝ)} (eN : (Fin n → ℝ) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (lam : Fin m.succ → ℝ) : (⇑eN '' ∑ i : Fin m.succ, if lam i = 0 then (C i).recessionCone else lam i • C i) = ∑ i : Fin m.succ, if lam i = 0 then (⇑eN '' C i).recessionCone else lam i • ⇑eN '' C i

Helper for Theorem 19.6: the weighted branch union in the tail coordinate transports through the Euclidean coordinate linear equivalence.

theorem helperForTheorem_19_6_preimage_weightedUnion_linearEquiv {n m : ℕ} {C : Fin m.succ → Set (Fin n → ℝ)} (eN : (Fin n → ℝ) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n)) (lam : Fin m.succ → ℝ) : (⇑eN ⁻¹' ∑ i : Fin m.succ, if lam i = 0 then (⇑eN '' C i).recessionCone else lam i • ⇑eN '' C i) = ∑ i : Fin m.succ, if lam i = 0 then (C i).recessionCone else lam i • C i

Helper for Theorem 19.6: transporting the weighted finite union formula back through a linear equivalence using preimage.

theorem helperForTheorem_19_6_convexConeHull_image_linearEquiv {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [Module ℝ α] [AddCommMonoid β] [Module ℝ β] (e : α ≃ₗ[ℝ] β) (s : Set α) : ⇑e '' ↑(ConvexCone.hull ℝ s) = ↑(ConvexCone.hull ℝ (⇑e '' s))

Helper for Theorem 19.6: linear equivalences transport convex-cone hulls through set image.

theorem helperForTheorem_19_6_cast_natAdd_one_eq_succ {n : ℕ} (i : Fin n) : Fin.cast ⋯ (Fin.natAdd 1 i) = i.succ

Helper for Theorem 19.6: after casting Fin.natAdd 1 i from Fin (1+n) to Fin (n+1), it coincides with Fin.succ i.

theorem helperForTheorem_19_6_tail_cast_natAdd_eq_tail_succ {n : ℕ} (v : Fin (n + 1) → ℝ) : (fun (i : Fin n) => v (Fin.cast ⋯ (Fin.natAdd 1 i))) = fun (i : Fin n) => v i.succ

Helper for Theorem 19.6: the tail-coordinate function written with casted Fin.natAdd 1 agrees with the usual Fin.succ tail function.