English
The direction of the affine span of s is the vectorSpan k s.
Русский
Направление афинного span множества s равно vectorSpan k s.
LaTeX
$$$\\operatorname{direction}(\\operatorname{affineSpan}_k s) = \\operatorname{vectorSpan}_k s$$$
Lean4
/-- The direction of the affine span is the `vectorSpan`. -/
theorem direction_affineSpan (s : Set P) : (affineSpan k s).direction = vectorSpan k s :=
by
apply le_antisymm
· refine Submodule.span_le.2 ?_
rintro v ⟨p₁, ⟨p₂, hp₂, v₁, hv₁, hp₁⟩, p₃, ⟨p₄, hp₄, v₂, hv₂, hp₃⟩, rfl⟩
simp only [SetLike.mem_coe]
rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]
exact (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂
· exact vectorSpan_mono k (subset_spanPoints k s)