English
For a nonempty subset s of P with a point p ∈ s, the vectorSpan of s equals the linear span of vectors p -ᵥ x for x ∈ s.
Русский
Для непустого множества s на P и точки p ∈ s вектор-распространение vectorSpan(s) равно линейному span множества векторов p -ᵥ x для x ∈ s.
LaTeX
$$$ vectorSpan_k(s) = span_k \\{ p -ᵥ x : x ∈ s \\} $$$
Lean4
/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the left. -/
theorem vectorSpan_eq_span_vsub_set_left {s : Set P} {p : P} (hp : p ∈ s) :
vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' s) :=
by
rw [vectorSpan_def]
refine le_antisymm ?_ (Submodule.span_mono ?_)
· rw [Submodule.span_le]
rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩
simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv
rw [← hv, SetLike.mem_coe, Submodule.mem_span]
exact fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)
· rintro v ⟨p₂, hp₂, hv⟩
exact ⟨p, hp, p₂, hp₂, hv⟩
