English
The vectorSpan of an indexed family equals the span of left subtractions with a fixed excluded index.
Русский
Вектор Span индексированного семейства равен span левых вычитаний с фиксированным исключённым индексом.
LaTeX
$$$ vectorSpan(k, Set.range p) = span_k (Set.range fun i => p i0 -ᵥ p i) $$$
Lean4
/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the left, excluding the subtraction of that point from itself. -/
theorem vectorSpan_range_eq_span_range_vsub_left_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_left_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⟩
