vectorSpan_pair_rev — Mathlib

English

The vector span of two points equals the subspace generated by their difference in the opposite order.

Русский

ВекторSpan двух точек равен подпространству, порождаемому их разностью в обратном порядке.

LaTeX

$$$\\operatorname{vectorSpan}_k(\\{p_1, p_2\\}) = \\operatorname{span}_k(p_2 - p_1)$$$

Lean4

/-- The `vectorSpan` of two points is the span of their difference (reversed). -/
theorem vectorSpan_pair_rev (p₁ p₂ : P) : vectorSpan k ({ p₁, p₂ } : Set P) = k ∙ p₂ -ᵥ p₁ := by
  rw [pair_comm, vectorSpan_pair]

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