vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints

English

The difference of two points in spanPoints lies in the vectorSpan.

Русский

Разность двух точек из spanPoints лежит в vectorSpan.

LaTeX

$$$p_1 \\in spanPoints(k,s) \\land p_2 \\in spanPoints(k,s) \\Rightarrow p_1 -_{\\mathrm{v}} p_2 \\in vectorSpan(k,s)$$$

Lean4

/-- Subtracting two points in the affine span produces a vector in the spanning submodule. -/
theorem vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints {s : Set P} {p₁ p₂ : P} (hp₁ : p₁ ∈ spanPoints k s)
    (hp₂ : p₂ ∈ spanPoints k s) : p₁ -ᵥ p₂ ∈ vectorSpan k s :=
  by
  rcases hp₁ with ⟨p₁a, ⟨hp₁a, ⟨v₁, ⟨hv₁, hv₁p⟩⟩⟩⟩
  rcases hp₂ with ⟨p₂a, ⟨hp₂a, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
  rw [hv₁p, hv₂p, vsub_vadd_eq_vsub_sub (v₁ +ᵥ p₁a), vadd_vsub_assoc, add_comm, add_sub_assoc]
  have hv₁v₂ : v₁ - v₂ ∈ vectorSpan k s := (vectorSpan k s).sub_mem hv₁ hv₂
  refine (vectorSpan k s).add_mem ?_ hv₁v₂
  exact vsub_mem_vectorSpan k hp₁a hp₂a

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