Documentation

Mathlib.Analysis.Convex.Radon

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.