affineSpan_insert_eq_affineSpan — Mathlib

English

If a point lies in the affine span of a set, inserting it does not change the span.

Русский

Если точка лежит в аффинной оболочке множества, добавление её не меняет оболочку.

LaTeX

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

Lean4

/-- If a point is in the affine span of a set, adding it to that set does not change the affine
span. -/
theorem affineSpan_insert_eq_affineSpan {p : P} {ps : Set P} (h : p ∈ affineSpan k ps) :
    affineSpan k (insert p ps) = affineSpan k ps :=
  by
  rw [← mem_coe] at h
  rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]

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