radon_partition

theorem radon_partition : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {f : ι → E}, ¬AffineIndependent 𝕜 f → ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty

The **Radon's theorem on convex sets** states that for any given family `f` of vectors in a vector space `E` over a linear ordered field `𝕜`, if the family is not affinely independent, then there exists a set `I` such that the convex hulls of `I` and the complement of `I` (denoted as `Iᶜ`) have a nonempty intersection. Here, a family is affinely independent if no nontrivial weighted subtractions (where the sum of weights is 0) result in the zero vector, and the convex hull of a set is the smallest convex set that contains the set.

More concisely: If a family of vectors in a vector space over a linear ordered field is not affinely independent, then their convex hulls have a nonempty intersection with the convex hull of their complement.