mem_vectorSpan_pair_rev — Mathlib

English

A vector lies in the vector span of two points iff it is a multiple of their reversed difference.

Русский

Вектор принадлежит векторному Span двух точек тогда и только тогда, когда он является кратной их разности в обратном порядке.

LaTeX

$$$v \\in \\operatorname{vectorSpan}_k(\\{p_1, p_2\\}) \\iff \\exists r \\in k,\\ r \\cdot (p_2 - p_1) = v$$$

Lean4

/-- A vector lies in the `vectorSpan` of two points if and only if it is a multiple of their
difference (reversed). -/
theorem mem_vectorSpan_pair_rev {p₁ p₂ : P} {v : V} :
    v ∈ vectorSpan k ({ p₁, p₂ } : Set P) ↔ ∃ r : k, r • (p₂ -ᵥ p₁) = v := by
  rw [vectorSpan_pair_rev, Submodule.mem_span_singleton]

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