vectorSpan_image_eq_span_vsub_set_left_ne

English

The vectorSpan of a range p is the span of left subtractions with a fixed left point i0.

Русский

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

LaTeX

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

Lean4

/-- The `vectorSpan` of the image of a function is the span of the pairwise subtractions with a
given point on the left, excluding the subtraction of that point from itself. -/
theorem vectorSpan_image_eq_span_vsub_set_left_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_left 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]

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