vadd_right_mem_affineSpan_pair — Mathlib

English

A vector added to the second point lies in the affine span of two points iff it is a multiple of their difference.

Русский

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

LaTeX

$$$v + p_2 \\in \\mathrm{line}[k, p_1, p_2] \\iff \\exists r \\in k,\\ r \\cdot (p_1 - p_2) = v$$$

Lean4

/-- A vector added to the second point lies in the affine span of two points if and only if it is
a multiple of their difference. -/
theorem vadd_right_mem_affineSpan_pair {p₁ p₂ : P} {v : V} : v +ᵥ p₂ ∈ line[k, p₁, p₂] ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v :=
  by rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan, mem_vectorSpan_pair]

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