vectorSpan_image_eq_span_vsub_set_right_ne

English

The vectorSpan of a range equals the span of right subtractions with a fixed right point i0.

Русский

Вектор Span диапазона равен span правых вычитаний с фиксированной правой точкой i0.

LaTeX

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

Lean4

/-- The `vectorSpan` of the image of a function is the span of the pairwise subtractions with a
given point on the right, excluding the subtraction of that point from itself. -/
theorem vectorSpan_image_eq_span_vsub_set_right_ne (p : ι → P) {s : Set ι} {i : ι} (hi : i ∈ s) :
    vectorSpan k (p '' s) = Submodule.span k ((· -ᵥ p i) '' (p '' (s \ { i }))) :=
  by
  conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
      Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

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