vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan

English

Adding a point in spanPoints to a vector in vectorSpan yields another point in spanPoints.

Русский

Прибавление точки из spanPoints к вектору из vectorSpan даёт новую точку в spanPoints.

LaTeX

$$$p \\in spanPoints(k,s) \\land v \\in vectorSpan(k,s) \\Rightarrow v +_{\\mathrm{v}} p \\in spanPoints(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_spanPoints_of_mem_spanPoints_of_mem_vectorSpan {s : Set P} {p : P} {v : V} (hp : p ∈ spanPoints k s)
    (hv : v ∈ vectorSpan k s) : v +ᵥ p ∈ spanPoints k s :=
  by
  rcases hp with ⟨p₂, ⟨hp₂, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
  rw [hv₂p, vadd_vadd]
  exact ⟨p₂, hp₂, v + v₂, (vectorSpan k s).add_mem hv hv₂, rfl⟩

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