vsub_mem_vectorSpan_pair — Mathlib

English

The difference between two points lies in the vector span of the two points.

Русский

Разность двух точек лежит в векторномspan двух точек.

LaTeX

$$$p_1 - \vec{p}_2 \in \mathrm{vectorSpan}(k, \{p_1,p_2\}).$$$

Lean4

/-- The difference between two points lies in their `vectorSpan`. -/
theorem vsub_mem_vectorSpan_pair (p₁ p₂ : P) : p₁ -ᵥ p₂ ∈ vectorSpan k ({ p₁, p₂ } : Set P) :=
  vsub_mem_vectorSpan _ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

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