vsub_rev_mem_vectorSpan_pair — Mathlib

English

The difference p2 - p1 lies in the vector span of {p1,p2}.

Русский

Разность p2 - p1 лежит в векторномspan множества {p1,p2}.

LaTeX

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

Lean4

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

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