English
Let p: ι → P be an indexed family in an affine space. Then the vector span of the range of p equals the span of all right-side differences p(i) − p(i0) for i ≠ i0, where i0 is a fixed index.
Русский
Пусть p : ι → P — семейство точек. Тогда векторное пространство, порождаемое образами p, совпадает с порождающим подпростраством всех векторов вида p(i) − p(i0) при i ≠ i0.
LaTeX
$$$\operatorname{vectorSpan}_k(\operatorname{Set.range} p) = \operatorname{Submodule.span}_k(\operatorname{Set.range} (\lambda i: { x // x \neq i_0 } \; \mapsto \; p i -_v p i_0))$$$
Lean4
/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the right, excluding the subtraction of that point from itself. -/
theorem vectorSpan_range_eq_span_range_vsub_right_ne (p : ι → P) (i₀ : ι) :
vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : { x // x ≠ i₀ } => p i -ᵥ p i₀) :=
by
rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_right_ne k _ (Set.mem_univ i₀)]
congr with v
simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists]
constructor
· rintro ⟨x, ⟨i₁, ⟨⟨_, hi₁⟩, rfl⟩⟩, hv⟩
exact ⟨i₁, hi₁, hv⟩
· exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩
