vectorSpan_eq_span_vsub_set_left_ne

English

The vectorSpan of a set s equals the span of right-subtractions p i -ᵥ p i0 for i in s.

Русский

Векторный охват множества s равен span векторов p(i) -ᵥ p(i0) для i ∈ s.

LaTeX

$$$ vectorSpan(k, Set.range p) = span_k (Set.range (λ i, p i -ᵥ p i0)) $$$

Lean4

/-- The `vectorSpan` is the span of the pairwise subtractions with a given point on the left,
excluding the subtraction of that point from itself. -/
theorem vectorSpan_eq_span_vsub_set_left_ne {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' (s \ { p })) :=
  by
  conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton,
      Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

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