vectorSpan_range_eq_span_range_vsub_left

English

The vectorSpan of a range equals the span of the pairwise left subtractions with a distinguished left index, excluding that index from the domain.

Русский

Вектор Span диапазона равен span парных левых вычитаний с выделенным левым индексом, исключая его из множества индексов.

LaTeX

$$$ vectorSpan(k, Set.range p) = span_k (Set.range fun i => vsub (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. -/
theorem vectorSpan_range_eq_span_range_vsub_left (p : ι → P) (i0 : ι) :
    vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i0 -ᵥ p i) :=
  by
  rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0), ← Set.range_comp]
  congr

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