theorem closure_cone_over_convexHull_eq_closure_sum_cones_succ (n m : ℕ) (C : Fin m.succ → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m.succ), (C i).Nonempty) (hCconv : ∀ (i : Fin m.succ), Convex ℝ (C i)) : have C0 := (convexHull ℝ) (⋃ (i : Fin m.succ), C i); have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S0 := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C0}; have K0 := ↑(ConvexCone.hull ℝ S0); have S := fun (i : Fin m.succ) => {v : EuclideanSpace ℝ (Fin (1 + n)) | 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 of the lifted cone over convexHull equals the closure of the sum of lifted cones when the index type is Fin (Nat.succ m).

theorem first_nonneg_of_mem_closure_lifted_cone {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C}; have K := ↑(ConvexCone.hull ℝ S); ∀ v ∈ closure K, 0 ≤ first v

Points in the closure of a lifted cone have nonnegative first coordinate.

theorem lifted_cone_nonempty {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C}; have K := ↑(ConvexCone.hull ℝ S); K.Nonempty

The lifted cone over a nonempty set is nonempty.

theorem lifted_cone_isConvexCone {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C}; have K := ↑(ConvexCone.hull ℝ S); IsConvexCone (1 + n) (⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ) '' K)

The coordinate image of a lifted cone is a convex cone.

theorem lineality_of_zero_sum_closure_lifted_cones {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hlineal : ∀ (z : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), z i ∈ (C i).recessionCone) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (C i).linealitySpace) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := fun (i : Fin m) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m) => ↑(ConvexCone.hull ℝ (S i)); ∀ (z : Fin m → EuclideanSpace ℝ (Fin (1 + n))), (∀ (i : Fin m), z i ∈ closure (K i)) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (closure (K i)).linealitySpace

Zero-sum families in closures of lifted cones are lineality directions.

theorem closure_sum_cones_eq_sum_closure_cones {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hlineal : ∀ (z : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), z i ∈ (C i).recessionCone) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (C i).linealitySpace) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := fun (i : Fin m) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m) => ↑(ConvexCone.hull ℝ (S i)); closure (∑ i : Fin m, K i) = ∑ i : Fin m, closure (K i)

Closure of the sum of lifted cones equals the sum of their closures.

theorem closure_lifted_cone_eq_closure_lifted_cone_closure {n : ℕ} (C0 : Set (EuclideanSpace ℝ (Fin n))) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S0 := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C0}; have K0 := ↑(ConvexCone.hull ℝ S0); have S0bar := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ closure C0}; have K0bar := ↑(ConvexCone.hull ℝ S0bar); closure K0 = closure K0bar

The closure of the lifted cone over C0 agrees with the closure of the lifted cone over closure C0.

theorem closure_C0_eq_first_one_slice_closure_lifted_cone {n : ℕ} {C0 : Set (EuclideanSpace ℝ (Fin n))} (hC0conv : Convex ℝ C0) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S0 := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C0}; have K0 := ↑(ConvexCone.hull ℝ S0); closure C0 = {x : EuclideanSpace ℝ (Fin n) | ∃ v ∈ closure K0, first v = 1 ∧ tail v = x}

The first = 1 slice of the closure of the lifted cone over C0 is closure C0.

theorem mem_sum_closure_cones_first_eq_one_iff {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := fun (i : Fin m) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m) => ↑(ConvexCone.hull ℝ (S i)); ∀ (v : EuclideanSpace ℝ (Fin (1 + n))), first v = 1 → (v ∈ ∑ i : Fin m, closure (K i) ↔ ∃ (lam : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ tail v ∈ ∑ i : Fin m, if lam i = 0 then (C i).recessionCone else lam i • C i)

The first = 1 slice of the sum of closures of lifted cones.

theorem mem_sum_closure_cones_first_eq_zero_iff {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) : have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := fun (i : Fin m) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i}; have K := fun (i : Fin m) => ↑(ConvexCone.hull ℝ (S i)); ∀ (v : EuclideanSpace ℝ (Fin (1 + n))), first v = 0 → (v ∈ ∑ i : Fin m, closure (K i) ↔ tail v ∈ ∑ i : Fin m, (C i).recessionCone)

The first = 0 slice of the sum of closures of lifted cones.