vadd_left_mem_affineSpan_pair — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- A vector added to the first point lies in the affine span of two points if and only if it is
a multiple of their difference. -/
theorem vadd_left_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 _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan, mem_vectorSpan_pair_rev]

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