theorem euclideanRelativeInterior_convexConeGenerated_eq (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) (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); euclideanRelativeInterior (1 + n) K = {v : EuclideanSpace ℝ (Fin (1 + n)) | 0 < first v ∧ tail v ∈ first v • euclideanRelativeInterior n C}

Corollary 6.8.1: Let C be a non-empty convex set in R^n, and let K be the convex cone in R^{n+1} generated by {(1, x) | x ∈ C}. Then ri K consists of the pairs (λ, x) such that λ > 0 and x ∈ λ ri C.