smul_vsub_rev_vadd_mem_affineSpan_pair

English

A scalar multiple of the other difference added to the second point lies in their affine span.

Русский

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

LaTeX

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

Lean4

/-- A multiple of the difference of two points added to the second point lies in their affine
span. -/
theorem smul_vsub_rev_vadd_mem_affineSpan_pair (r : k) (p₁ p₂ : P) : r • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ line[k, p₁, p₂] :=
  AffineMap.lineMap_rev_mem_affineSpan_pair _ _ _

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