vectorSpan_eq_span_vsub_set_right_ne

English

The vectorSpan of a set s with a distinguished point p equals the span of right-subtractions p i -ᵥ p i0 for i ≠ i0, reflecting exclusion of the base point.

Русский

Векторный охват множества s с выделенной точкой p равен span векторов p i -ᵥ p i0 для i ≠ i0, исключая базовую точку.

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 right,
excluding the subtraction of that point from itself. -/
theorem vectorSpan_eq_span_vsub_set_right_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_right k hp, ← Set.insert_eq_of_mem hp, ← Set.insert_diff_singleton,
      Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

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