Existing in Mathlib · Geometry
Radon's Theorem
Whenever an indexed family of points has an affine dependence, its indices can be divided into a set and its complement so that the convex hulls generated by the two groups share at least one point.
- affine dependence
- convex hulls
- Radon partitions
- center of mass
- convex geometry
Exact theorem
Exact Mathlib statement
theorem Convex.radon_partition {ι 𝕜 E : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : ι → E} (h : ¬ AffineIndependent 𝕜 f) : ∃ I, (convexHull 𝕜 (f '' I) ∩ convexHull 𝕜 (f '' Iᶜ)).NonemptyThe theorem at a glance
Radon's Theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Radon's Theorem at a glance
Detailed visual description
A four-point convex-position example makes the endpoint concrete: alternating antique-gold and cobalt sign classes determine two crossing hull segments. A four-stage source-faithful route extracts an affine relation, separates coefficient signs, constructs one center of mass, and places it in both hulls, while the footer preserves the declaration's non-dimensional starting point.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Radon's Theorem — scientific diagram
Detailed visual description
This page indexes Mathlib's affine-dependence form of Radon's theorem for an indexed family in a module over the source's linearly ordered field typeclasses. From failure of affine independence it obtains a set I of indices whose image convex hull intersects the image convex hull of I's complement. The selected declaration does not assume finite dimensionality and does not directly state the familiar d+2-points-in-d-dimensions corollary. It asserts existence only, not a canonical or unique partition, a unique intersection point, or a computation.
Why it matters
A mathematical landmark
Radon's theorem is a foundational partition principle in convex geometry and a key engine behind Helly-type local-to-global results. Mathlib's source proof makes the geometry explicit: an affine relation is split by coefficient sign, and the same center of mass is placed in both complementary convex hulls.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's affine-dependence form of Radon's theorem for an indexed family in a module over the source's linearly ordered field typeclasses. From failure of affine independence it obtains a set I of indices whose image convex hull intersects the image convex hull of I's complement. The selected declaration does not assume finite dimensionality and does not directly state the familiar d+2-points-in-d-dimensions corollary. It asserts existence only, not a canonical or unique partition, a unique intersection point, or a computation.
- ProofAtlas did not originate Radon's theorem or Mathlib's declaration.
- The selected declaration begins with affine dependence; it is not itself stated with a finite-dimensional or d+2-point hypothesis.
- The theorem does not compute a partition or common point and does not assert uniqueness or canonicity.
- The selected declaration is not Helly's theorem.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Convex.radon_partitionin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.radon-theorem.v001