Closed finitely generated cones

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.mem_pointedCone_hull_range_iff {I : Type u_1} {E : Type u_2} [Fintype I] [AddCommGroup E] [Module ℝ E] (A : I → E) (x : E) : x ∈ PointedCone.hull ℝ (Set.range A) ↔ ∃ (c : I → ℝ), (∀ (i : I), 0 ≤ c i) ∧ ∑ i : I, c i • A i = x

A finite conic combination is a sum with nonnegative coefficients.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.isClosed_pointedCone_hull_range_of_linearIndependent {I : Type u_1} {E : Type u_2} [Finite I] [NormedAddCommGroup E] [NormedSpace ℝ E] (A : I → E) (hA : LinearIndependent ℝ A) : IsClosed ↑(PointedCone.hull ℝ (Set.range A))

The cone spanned by a finite linearly independent family is closed.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.isClosed_pointedCone_hull_range {I : Type u_1} {E : Type u_2} [Finite I] [NormedAddCommGroup E] [NormedSpace ℝ E] (A : I → E) : IsClosed ↑(PointedCone.hull ℝ (Set.range A))

A cone generated by a finite family of real vectors is closed.