vectorSpan_pair — Mathlib

English

The vector span of two points is the subspace generated by their difference.

Русский

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

LaTeX

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

Lean4

/-- The `vectorSpan` of two points is the span of their difference. -/
theorem vectorSpan_pair (p₁ p₂ : P) : vectorSpan k ({ p₁, p₂ } : Set P) = k ∙ p₁ -ᵥ p₂ := by
  simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self, Submodule.span_insert_zero]

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