# 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 nontrivially.

As a corollary, we prove Helly's theorem, which is a basic result in discrete geometry on the
intersection of convex sets. Let `X₁, ⋯, Xₙ`

be a finite family of convex sets in `ℝᵈ`

with
`n ≥ d + 1`

. The theorem states that if any `d + 1`

sets from this family intersect nontrivially,
then the whole family intersect nontrivially. For the infinite family of sets it is not true, as
example of `Set.Ioo 0 (1 / n)`

for `n : ℕ`

shows. But the statement is true, if we assume
compactness of sets (see `helly_theorem_compact`

)

## Tags #

convex hull, affine independence, Radon, Helly

**Radon's 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 nontrivially.

**Helly's theorem** for finite families of convex sets.

If `F`

is a finite family of convex sets in a vector space of finite dimension `d`

, and any
`k ≤ d + 1`

sets of `F`

intersect nontrivially, then all sets of `F`

intersect nontrivially.

**Helly's theorem** for finite families of convex sets in its classical form.

If `F`

is a family of `n`

convex sets in a vector space of finite dimension `d`

, with `n ≥ d + 1`

,
and any `d + 1`

sets of `F`

intersect nontrivially, then all sets of `F`

intersect nontrivially.

**Helly's theorem** for finite sets of convex sets.

If `F`

is a finite set of convex sets in a vector space of finite dimension `d`

, and any `k ≤ d + 1`

sets from `F`

intersect nontrivially, then all sets from `F`

intersect nontrivially.

**Helly's theorem** for finite sets of convex sets in its classical form.

If `F`

is a finite set of convex sets in a vector space of finite dimension `d`

, with `n ≥ d + 1`

,
and any `d + 1`

sets from `F`

intersect nontrivially,
then all sets from `F`

intersect nontrivially.

**Helly's theorem** for families of compact convex sets.

If `F`

is a family of compact convex sets in a vector space of finite dimension `d`

, and any
`k ≤ d + 1`

sets of `F`

intersect nontrivially, then all sets of `F`

intersect nontrivially.

**Helly's theorem** for families of compact convex sets in its classical form.

If `F`

is a (possibly infinite) family of more than `d + 1`

compact convex sets in a vector space of
finite dimension `d`

, and any `d + 1`

sets of `F`

intersect nontrivially,
then all sets of `F`

intersect nontrivially.

**Helly's theorem** for sets of compact convex sets.

If `F`

is a set of compact convex sets in a vector space of finite dimension `d`

, and any
`k ≤ d + 1`

sets from `F`

intersect nontrivially, then all sets from `F`

intersect nontrivially.

**Helly's theorem** for sets of compact convex sets in its classical version.

If `F`

is a (possibly infinite) set of more than `d + 1`

compact convex sets in a vector space of
finite dimension `d`

, and any `d + 1`

sets from `F`

intersect nontrivially,
then all sets from `F`

intersect nontrivially.