vectorSpan_range_eq_span_range_vsub_right

English

The vectorSpan of an indexed family is the span of right subtractions with a fixed right index, excluding that index.

Русский

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

LaTeX

$$$ vectorSpan(k, Set.range p) = span_k (Set.range fun i => vsub (p i) (p i0)) $$$

Lean4

/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the right. -/
theorem vectorSpan_range_eq_span_range_vsub_right (p : ι → P) (i0 : ι) :
    vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i -ᵥ p i0) :=
  by
  rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_range_self i0), ← Set.range_comp]
  congr

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