English
If a family is affinely independent, replacing any one point by a new point not in the affine span of the rest preserves affine independence.
Русский
Если семейство аффинно независимо, замена любой точки на новую, которая не лежит в аффine-обобщении остальных точек, сохраняет аффинную независимость.
LaTeX
$$$\\text{AffineIndependent}_k(p) \\Rightarrow \\forall i,\\ p_0:\\ P\\, (p_0 \\notin \\operatorname{affineSpan}_k(p''{\\{x\\mid x\\ne i\\}})) \\Rightarrow \\text{AffineIndependent}_k(\\mathrm{update}\\ p\\ i\\ p_0).$$$
Lean4
/-- If a family is affinely independent, we update any one point with a new point does not lie in
the affine span of that family, the new family is affinely independent. -/
theorem affineIndependent_update_of_notMem_affineSpan [DecidableEq ι] {p : ι → P} (ha : AffineIndependent k p) {i : ι}
{p₀ : P} (hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})) : AffineIndependent k (Function.update p i p₀) :=
by
set f : ι → P := Function.update p i p₀ with hf
have h₁ : (fun x : {x | x ≠ i} ↦ p x) = fun x : {x | x ≠ i} ↦ f x := by ext x; aesop
have h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i} := Set.image_congr <| by simpa using congr_fun h₁
replace ha : AffineIndependent k fun x : {x | x ≠ i} ↦ f x := h₁ ▸ AffineIndependent.subtype ha _
exact AffineIndependent.affineIndependent_of_notMem_span ha <| by aesop
