vectorSpan_insert_eq_vectorSpan — Mathlib

English

Let p be in the affine span of ps. Then adding p to ps does not change the vector span: vectorSpan k (insert p ps) = vectorSpan k ps.

Русский

Пусть p принадлежит аффинному охвату affineSpan k ps. Тогда добавление p в ps не изменяет векторный охват: vectorSpan k (insert p ps) = vectorSpan k ps.

LaTeX

$$$p \in \operatorname{affineSpan}(k, ps) \Rightarrow \operatorname{vectorSpan} k(\mathrm{insert}\;p\;ps) = \operatorname{vectorSpan} k\;ps$$$

Lean4

/-- If a point is in the affine span of a set, adding it to that set does not change the vector
span. -/
theorem vectorSpan_insert_eq_vectorSpan {p : P} {ps : Set P} (h : p ∈ affineSpan k ps) :
    vectorSpan k (insert p ps) = vectorSpan k ps := by
  simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]

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