English
If a family is affinely independent, and the spans of points indexed by two subsets share a point, then the two index subsets intersect.
Русский
Если семейство аффинно независимо, и выпуклые оболочки точек, индексируемых двумя подмножествами, пересекаются, то множества индексов пересекаются.
LaTeX
$$$\\forall p\\, ha:\\ affineIndependent\\ k\\ p\\; \\forall s_1,s_2: Set\\ ι,\\; \\exists i\\in s_1\\cap s_2: \\text{— условие пересечения} $$$
Lean4
/-- If a family is affinely independent, and the spans of points
indexed by two subsets of the index type have a point in common, those
subsets of the index type have an element in common, if the underlying
ring is nontrivial. -/
theorem exists_mem_inter_of_exists_mem_inter_affineSpan [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p)
{s1 s2 : Set ι} {p0 : P} (hp0s1 : p0 ∈ affineSpan k (p '' s1)) (hp0s2 : p0 ∈ affineSpan k (p '' s2)) :
∃ i : ι, i ∈ s1 ∩ s2 := by
rw [Set.image_eq_range] at hp0s1 hp0s2
rw [mem_affineSpan_iff_eq_affineCombination, ←
Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype] at hp0s1 hp0s2
rcases hp0s1 with ⟨fs1, hfs1, w1, hw1, hp0s1⟩
rcases hp0s2 with ⟨fs2, hfs2, w2, hw2, hp0s2⟩
rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
replace ha := ha fs1 fs2 w1 w2 hw1 hw2 (hp0s1 ▸ hp0s2)
have hnz : ∑ i ∈ fs1, w1 i ≠ 0 := hw1.symm ▸ one_ne_zero
rcases Finset.exists_ne_zero_of_sum_ne_zero hnz with ⟨i, hifs1, hinz⟩
simp_rw [← Set.indicator_of_mem (Finset.mem_coe.2 hifs1) w1, ha] at hinz
use i, hfs1 hifs1
exact hfs2 (Set.mem_of_indicator_ne_zero hinz)
