vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan

English

Subtracting two points in the affine span yields a vector in vectorSpan k s.

Русский

Разность двух точек из афинного span дает вектор из vectorSpan k s.

LaTeX

$$$p_1 \\in \\operatorname{affineSpan}_k s \\land p_2 \\in \\operatorname{affineSpan}_k s \\Rightarrow p_1 -\\!\\! v p_2 \\in \\operatorname{vectorSpan}_k s$$$

Lean4

/-- Subtracting two points in the affine span produces a vector in the spanning submodule. -/
theorem vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan {s : Set P} {p₁ p₂ : P} (hp₁ : p₁ ∈ affineSpan k s)
    (hp₂ : p₂ ∈ affineSpan k s) : p₁ -ᵥ p₂ ∈ vectorSpan k s :=
  vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints k hp₁ hp₂

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