mem_vectorSpan_pair — Mathlib

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]

Похожие утверждения