affineSpan_insert_affineSpan — Mathlib

English

The same invariance as before holds for insertion of a point into an existing span.

Русский

Та же инвариантность сохраняется при добавлении точки к существующей оболочке.

LaTeX

$$$\operatorname{affineSpan}(k, (\text{insert } p (\operatorname{affineSpan}(k, ps) : \text{Set} P))) = \operatorname{affineSpan}(k, (\text{insert } p ps)).$$$

Lean4

/-- Taking the affine span of a set, adding a point and taking the span again produces the same
results as adding the point to the set and taking the span. -/
theorem affineSpan_insert_affineSpan (p : P) (ps : Set P) :
    affineSpan k (insert p (affineSpan k ps : Set P)) = affineSpan k (insert p ps) := by
  rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]

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