theorem exists_t_of_fm_constraints {m : ℕ} (c d : Fin m → ℝ) (hfm_zero : ∀ (k : Fin m), c k = 0 → 0 ≤ d k) (hfm_pair : ∀ (i j : Fin m), c i > 0 → c j < 0 → -c j * d i + c i * d j ≥ 0) : ∃ (t : ℝ), ∀ (i : Fin m), c i * t ≤ d i

theorem polyhedron_projection {n m : ℕ} (C : Matrix (Fin m) (Fin n) ℝ) (c d : Fin m → ℝ) : ∃ (m' : ℕ) (A' : Matrix (Fin m') (Fin n) ℝ) (b' : Fin m' → ℝ), {y : EuclideanSpace ℝ (Fin n) | ∃ (t : ℝ), ∀ (i : Fin m), ∑ j : Fin n, C i j * y.ofLp j + c i * t ≤ d i} = {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin m'), ∑ j : Fin n, A' i j * y.ofLp j ≤ b' i}

theorem convexHull_polyhedron_point_eq_projection {n m : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (v : EuclideanSpace ℝ (Fin n)) (hP : ∃ (x : EuclideanSpace ℝ (Fin n)), ∀ (i : Fin m), ∑ j : Fin n, A i j * x.ofLp j ≤ b i) (hbdd : ∀ (d : EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), ∑ j : Fin n, A i j * d.ofLp j ≤ 0) → d = 0) : ∃ (m₁ : ℕ) (C : Matrix (Fin m₁) (Fin n) ℝ) (c : Fin m₁ → ℝ) (d : Fin m₁ → ℝ), (convexHull ℝ) ({x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin m), ∑ j : Fin n, A i j * x.ofLp j ≤ b i} ∪ {v}) = {y : EuclideanSpace ℝ (Fin n) | ∃ (t : ℝ), ∀ (i : Fin m₁), ∑ j : Fin n, C i j * y.ofLp j + c i * t ≤ d i}

theorem polyhedron_convex_hull_point {n m : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (v : EuclideanSpace ℝ (Fin n)) (hP : ∃ (x : EuclideanSpace ℝ (Fin n)), ∀ (i : Fin m), ∑ j : Fin n, A i j * x.ofLp j ≤ b i) (hbdd : ∀ (d : EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), ∑ j : Fin n, A i j * d.ofLp j ≤ 0) → d = 0) : ∃ (m' : ℕ) (A' : Matrix (Fin m') (Fin n) ℝ) (b' : Fin m' → ℝ), (convexHull ℝ) ({x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin m), ∑ j : Fin n, A i j * x.ofLp j ≤ b i} ∪ {v}) = {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin m'), ∑ j : Fin n, A' i j * x.ofLp j ≤ b' i}

theorem polytope_trivial_recession_cone {n : ℕ} (S : Finset (EuclideanSpace ℝ (Fin n))) (hS : S.Nonempty) {m : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (hAb : (convexHull ℝ) ↑S = {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin m), ∑ j : Fin n, A i j * x.ofLp j ≤ b i}) (d : EuclideanSpace ℝ (Fin n)) : (∀ (i : Fin m), ∑ j : Fin n, A i j * d.ofLp j ≤ 0) → d = 0

theorem minkowski_weyl {n : ℕ} (S : Finset (EuclideanSpace ℝ (Fin n))) (hS : S.Nonempty) : ∃ (m : ℕ) (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ), (convexHull ℝ) ↑S = {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin m), ∑ j : Fin n, A i j * x.ofLp j ≤ b i}