English
For affinely independent p, p(i) ∈ affineSpan(k, p''s) iff i ∈ s.
Русский
Если p аффинно независимо, то p(i) принадлежит аффинной оболочке p''s тогда и только тогда, когда i ∈ s.
LaTeX
$$$\\operatorname{AffineIndependent} k p \\Rightarrow \\forall i\\in ι, s \\subseteq ι,\\; p(i)\\in affineSpan k (p''s) \\iff i\\in s$$$
Lean4
/-- If a family is affinely independent, a point in the family is in
the span of some of the points given by a subset of the index type if
and only if that point's index is in the subset, if the underlying
ring is nontrivial. -/
@[simp]
protected theorem mem_affineSpan_iff [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) :
p i ∈ affineSpan k (p '' s) ↔ i ∈ s := by
constructor
· intro hs
have h :=
AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
(mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))
rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h
· exact fun h => mem_affineSpan k (Set.mem_image_of_mem p h)
