case mp
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) → ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w

case mpr
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ (∃ s w x, p1 = ↑(Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
constructor
no goals
case mp
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) → ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
exact eq_affineCombination_of_mem_affineSpan
case mpr.intro.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
case mpr
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ (∃ s w x, p1 = ↑(Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)
rintro ⟨s, w, hw, rfl⟩
no goals
case mpr.intro.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
exact affineCombination_mem_affineSpan hw p