k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑(affineSpan k s)) } ≤ finrank k { x // x ∈ vectorSpan k s } + 1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ vectorSpan k (insert p s) } ≤ finrank k { x // x ∈ vectorSpan k s } + 1
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ direction (affineSpan k s) } ≤ finrank k { x // x ∈ vectorSpan k s }
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ vectorSpan k (insert p ↑(affineSpan k s)) } ≤ finrank k { x // x ∈ vectorSpan k s } + 1
refine' (finrank_vectorSpan_insert_le _ _).trans (add_le_add_right _ _)
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k { x // x ∈ direction (affineSpan k s) } ≤ finrank k { x // x ∈ vectorSpan k s }
rw [direction_affineSpan]