k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k (Set.range p) ≤ sp
hc : Finset.card Finset.univ = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k (Set.range p) = sp
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k (Set.range p) = sp
rw [← Finset.card_univ] at hc
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle✝¹ : affineSpan k (p '' Set.univ) ≤ sp
hle✝ : affineSpan k (p '' ↑Finset.univ) ≤ sp
hle : affineSpan k ↑(Finset.image p Finset.univ) ≤ sp
hc : Finset.card Finset.univ = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k ↑(Finset.image p Finset.univ) = sp
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle : affineSpan k (Set.range p) ≤ sp
hc : Finset.card Finset.univ = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k (Set.range p) = sp
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle⊢
no goals
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k { x // x ∈ direction sp }
hle✝¹ : affineSpan k (p '' Set.univ) ≤ sp
hle✝ : affineSpan k (p '' ↑Finset.univ) ≤ sp
hle : affineSpan k ↑(Finset.image p Finset.univ) ≤ sp
hc : Finset.card Finset.univ = finrank k { x // x ∈ direction sp } + 1
⊢ affineSpan k ↑(Finset.image p Finset.univ) = sp
exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc