smul_vsub_rev_mem_vectorSpan_pair

English

A scalar multiple of the reversed difference lies in the vector span.

Русский

Умножение на скаляр разности в обратном порядке принадлежит векторному span.

LaTeX

$$$r \cdot (p_2 - p_1) \in \mathrm{vectorSpan}(k, \{p_1,p_2\}).$$$

Lean4

/-- A multiple of the difference between two points (reversed) lies in their `vectorSpan`. -/
theorem smul_vsub_rev_mem_vectorSpan_pair (r : k) (p₁ p₂ : P) : r • (p₂ -ᵥ p₁) ∈ vectorSpan k ({ p₁, p₂ } : Set P) :=
  Submodule.smul_mem _ _ (vsub_rev_mem_vectorSpan_pair k p₁ p₂)

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