vsub_mem_vectorSpan — Mathlib

English

Let s be a subset of points in an affine space. Then for any p1, p2 in s, the affine difference p1 −ᵥ p2 lies in the vector span of s.

Русский

Пусть s — подмножество точек в аффинном пространстве. Тогда для любых p1, p2 ∈ s разность p1 −ᵥ p2 принадлежит векторной оболочке s.

LaTeX

$$$\\forall k, V, P, (\\text{Ring } k), (\\text{AddCommGroup } V), (\\text{Module } k V), (\\text{AffineSpace } V P), \\forall s \\subseteq P, \\forall p_1,p_2 \\in s:\\ p_1 -_{\\mathrm{v}} p_2 \\in \\operatorname{vectorSpan} k\, s$$$

Lean4

/-- Each pairwise difference is in the `vectorSpan`. -/
theorem vsub_mem_vectorSpan {s : Set P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : p₁ -ᵥ p₂ ∈ vectorSpan k s :=
  vsub_set_subset_vectorSpan k s (vsub_mem_vsub hp₁ hp₂)

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