@[simp]

theorem AffineSpace.vectorSpan_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) (v : V) : vectorSpan k (v +ᵥ s) = vectorSpan k s