no goals
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ vectorSpan k ∅ = ⊥
rw [vectorSpan_def, vsub_empty, Submodule.span_empty]