notMem_affineSpan_diff — Mathlib

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]

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