theorem weightedVSub_mem_vectorSpan' {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : ι → P} {w : ι → k} {s : Finset ι} {t : Set P} (h : ∑ i ∈ s, w i = 0) (hp : ∀ i ∈ s, p i ∈ t) : (s.weightedVSub p) w ∈ vectorSpan k t

theorem affineCombination_mem_affineSpan' {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : ι → P} {w : ι → k} {s : Finset ι} {t : Set P} [Nontrivial k] (h : ∑ i ∈ s, w i = 1) (hp : ∀ i ∈ s, p i ∈ t) : (Finset.affineCombination k s p) w ∈ affineSpan k t

theorem mem_affineSpan_image {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₀ : P} {p : ι → P} {s : Finset ι} [Nontrivial k] : p₀ ∈ affineSpan k (p '' ↑s) ↔ ∃ (w : ι → k), ∑ i ∈ s, w i = 1 ∧ p₀ = (Finset.affineCombination k s p) w