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]