vectorSpan_eq_span_vsub_finset_right_ne

English

For a finite set, the vectorSpan of its image equals the span of right-subtractions (excluding the base index) in finite form.

Русский

Для конечного множества векторSpan образа равно span правых вычитаний (кроме базового индекса) в конечной форме.

LaTeX

$$$ vectorSpan(k, s.toSet) = span_k ((s.erase p).image (λ x, x -ᵥ p)) $$$

Lean4

/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the right,
excluding the subtraction of that point from itself. -/
theorem vectorSpan_eq_span_vsub_finset_right_ne [DecidableEq P] [DecidableEq V] {s : Finset P} {p : P} (hp : p ∈ s) :
    vectorSpan k (s : Set P) = Submodule.span k ((s.erase p).image (· -ᵥ p)) := by
  simp [vectorSpan_eq_span_vsub_set_right_ne _ (Finset.mem_coe.mpr hp)]

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