English
A vector lies in the vector span of two points if and only if it is a scalar multiple of their difference.
Русский
Вектор принадлежит векторному Span двух точек тогда и только тогда, когда он является скалярным кратным их разности.
LaTeX
$$$v \\in \\operatorname{vectorSpan}_k(\\{p_1, p_2\\}) \\iff \\exists r \\in k,\\ r \\cdot (p_1 - p_2) = v$$$
Lean4
/-- A vector lies in the `vectorSpan` of two points if and only if it is a multiple of their
difference. -/
theorem mem_vectorSpan_pair {p₁ p₂ : P} {v : V} : v ∈ vectorSpan k ({ p₁, p₂ } : Set P) ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v :=
by rw [vectorSpan_pair, Submodule.mem_span_singleton]