Radon's theorem on convex sets

Radon's theorem states that any affine dependent set can be partitioned into two sets whose convex hulls intersect.

Tags

convex hull, radon, affine independence

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

Radon theorem on convex sets: Any family f of affine dependent vectors contains a set I with the property that convex hulls of I and Iᶜ intersect.