English
If a family is affinely independent, then a given point p_i is not in the affine span of the rest of the family when restricting away i.
Русский
Если семейство аффинно независимо, то точка p_i не лежит в аффинной оболочке остальных точек при исключении i.
LaTeX
$$$\\forall i\\; \\forall s\\; \\text{- тождество формула: } p_i \\notin affineSpan k (p''(s\\setminus\\{i\\}))$$$
Lean4
/-- If a family is affinely independent, a point in the family is not
in the affine span of the other points, if the underlying ring is
nontrivial. -/
theorem notMem_affineSpan_diff [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) :
p i ∉ affineSpan k (p '' (s \ { i })) := by simp [ha]