Independent generators for a finite conical combination

Every conical combination can be expressed using a linearly independent subfamily of its original generators.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nonneg_representation_linearIndependent {I : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] (A : I → E) (s : Finset I) (w : I → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) : ∃ t ⊆ s, (LinearIndependent ℝ fun (i : ↥t) => A ↑i) ∧ ∃ (v : I → ℝ), (∀ i ∈ t, 0 ≤ v i) ∧ ∑ i ∈ t, v i • A i = ∑ i ∈ s, w i • A i

A nonnegative finite combination uses a linearly independent subfamily after possibly changing its coefficients.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_linearIndependent_subcone {I : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Finite I] (A : I → E) {x : E} (hx : x ∈ PointedCone.hull ℝ (Set.range A)) : ∃ (s : Finset I), (LinearIndependent ℝ fun (i : ↥s) => A ↑i) ∧ x ∈ PointedCone.hull ℝ (Set.range fun (i : ↥s) => A ↑i)

Every element of a finitely generated cone belongs to the cone generated by some linearly independent subfamily of the given generators.