vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan

English

Adding a point in the affine span to a vector in the spanning submodule yields a point in the affine span.

Русский

Прибавление вектора к точке афинного span дает точку в афинном span.

LaTeX

$$$hp : p \\in \\operatorname{affineSpan}_k s \land hv : v \\in \\operatorname{vectorSpan}_k s \\Rightarrow v +\\!\\! p \\in \\operatorname{affineSpan}_k s$$$

Lean4

/-- Adding a point in the affine span and a vector in the spanning submodule produces a point in the
affine span. -/
theorem vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan {s : Set P} {p : P} {v : V} (hp : p ∈ affineSpan k s)
    (hv : v ∈ vectorSpan k s) : v +ᵥ p ∈ affineSpan k s :=
  vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan k hp hv

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