English
If a family is affinely independent and s1, s2 are disjoint, then the corresponding affine spans are disjoint.
Русский
Если семейство аффинно независимо, и множества s1, s2 не пересекаются, то их аффинные оболочки не пересекаются.
LaTeX
$$$\\operatorname{Disjoint} s1 s2\\; \\Rightarrow\\; \\operatorname{Disjoint}(\\operatorname{affineSpan} k (p''s1), \\operatorname{affineSpan} k (p''s2))$$$
Lean4
/-- If a family is affinely independent, the spans of points indexed
by disjoint subsets of the index type are disjoint, if the underlying
ring is nontrivial. -/
theorem affineSpan_disjoint_of_disjoint [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) {s1 s2 : Set ι}
(hd : Disjoint s1 s2) : Disjoint (affineSpan k (p '' s1) : Set P) (affineSpan k (p '' s2)) :=
by
refine Set.disjoint_left.2 fun p0 hp0s1 hp0s2 => ?_
obtain ⟨i, hi⟩ := ha.exists_mem_inter_of_exists_mem_inter_affineSpan hp0s1 hp0s2
exact Set.disjoint_iff.1 hd hi
