theorem helperForTheorem_19_1_liftFiniteGeneration_from_projection {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) (hCne : C.Nonempty) {L W : Submodule ℝ (Fin n → ℝ)} (hWL : IsCompl W L) {π : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ} (hker : LinearMap.ker π = L) (hrange : LinearMap.range π = W) (hprojW : ∀ w ∈ W, π w = w) (hL : ↑L = linealitySpace_fin C) : have K := ⇑π '' C; IsFinitelyGeneratedConvexSet n K → (∃ (SL : Set (Fin n → ℝ)), SL.Finite ∧ SL ⊆ ↑L ∧ ↑L ⊆ cone n SL) → IsFinitelyGeneratedConvexSet n C

Helper for Theorem 19.1: lift finite generation along a lineality projection.

theorem helperForTheorem_19_1_closed_finiteFaces_imp_finitelyGenerated_via_linealitySplit {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) : IsClosed C ∧ {C' : Set (Fin n → ℝ) | IsFace C C'}.Finite → IsFinitelyGeneratedConvexSet n C

Helper for Theorem 19.1: closed convex sets with finitely many faces are finitely generated, via a lineality split.

theorem helperForTheorem_19_1_closed_finiteFaces_imp_finitelyGenerated {n : ℕ} {C : Set (Fin n → ℝ)} (hc : Convex ℝ C) : IsClosed C ∧ {C' : Set (Fin n → ℝ) | IsFace C C'}.Finite → IsFinitelyGeneratedConvexSet n C

Helper for Theorem 19.1: closed convex sets with finitely many faces are finitely generated.

theorem helperForTheorem_19_1_dotProduct_lift_split {n : ℕ} (x : Fin n → ℝ) (b : Fin (n + 1) → ℝ) : (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ⬝ᵥ b = b 0 + x ⬝ᵥ fun (i : Fin n) => b i.succ

Helper for Theorem 19.1: split the dot-product with a lifted vector.

theorem helperForTheorem_19_1_liftingHyperplane_eq_set (n : ℕ) : liftingHyperplane n = {y : Fin (n + 1) → ℝ | y 0 = 1}

Helper for Theorem 19.1: the lifting hyperplane is the set of points with first coordinate 1.

theorem helperForTheorem_19_1_lift_preimage_closedHalfSpaceLE {n : ℕ} (b : Fin (n + 1) → ℝ) (β : ℝ) : {x : Fin n → ℝ | (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ closedHalfSpaceLE (n + 1) b β} = closedHalfSpaceLE n (fun (i : Fin n) => b i.succ) (β - b 0)

Helper for Theorem 19.1: preimage of a closed half-space under the lift map.

theorem helperForTheorem_19_1_liftingHyperplane_polyhedral (n : ℕ) : IsPolyhedralConvexSet (n + 1) (liftingHyperplane n)

Helper for Theorem 19.1: the lifting hyperplane is polyhedral.

theorem helperForTheorem_19_1_polyhedral_inter {n : ℕ} {C D : Set (Fin n → ℝ)} (hC : IsPolyhedralConvexSet n C) (hD : IsPolyhedralConvexSet n D) : IsPolyhedralConvexSet n (C ∩ D)

Helper for Theorem 19.1: intersection of polyhedral convex sets is polyhedral.

theorem helperForTheorem_19_1_lift_preimage_polyhedral {n : ℕ} {K : Set (Fin (n + 1) → ℝ)} (hK : IsPolyhedralConvexSet (n + 1) K) : IsPolyhedralConvexSet n {x : Fin n → ℝ | (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ K}

Helper for Theorem 19.1: pull back a polyhedral set under the lift map.

theorem helperForTheorem_19_1_cone_polar_eq_iInter_halfspaces {m : ℕ} {T : Set (Fin m → ℝ)} : {xStar : Fin m → ℝ | ∀ x ∈ cone m T, x ⬝ᵥ xStar ≤ 0} = ⋂ t ∈ T, closedHalfSpaceLE m t 0

Helper for Theorem 19.1: polar of a generated cone is a half-space intersection.

theorem helperForTheorem_19_1_exists_t_pos_of_neg_offset_pos_slope {a b : ℝ} (ha : a ≤ 0) (hb : 0 < b) : ∃ (t : ℝ), 0 ≤ t ∧ 0 < a + t * b

Helper for Theorem 19.1: choose a nonnegative t so a + t * b is positive.

theorem helperForTheorem_19_1_polar_of_mixedConvexHull_eq_iInter {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hS₀ne : S₀.Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ mixedConvexHull S₀ S₁, x ⬝ᵥ xStar ≤ 0} = (⋂ s ∈ S₀, closedHalfSpaceLE n s 0) ∩ ⋂ d ∈ S₁, closedHalfSpaceLE n d 0

Helper for Theorem 19.1: polar of a mixed convex hull is an intersection of half-spaces.

theorem helperForTheorem_19_1_isClosed_simplicialCone_of_linearIndependent {m k : ℕ} (v : Fin k → Fin m → ℝ) (hlin : LinearIndependent ℝ v) : IsClosed {x : Fin m → ℝ | ∃ (c : Fin k → ℝ), (∀ (i : Fin k), 0 ≤ c i) ∧ x = ∑ i : Fin k, c i • v i}

Helper for Theorem 19.1: simplicial cones are closed.

theorem helperForTheorem_19_1_isClosed_cone_of_finite_generators {m : ℕ} {T : Set (Fin m → ℝ)} (hT : T.Finite) : IsClosed (cone m T)

Helper for Theorem 19.1: finitely generated cones are closed.

theorem helperForTheorem_19_1_zero_set_polyhedral {m : ℕ} : IsPolyhedralConvexSet m {0}

Helper for Theorem 19.1: the singleton {0} is polyhedral.