Converse of Mathlib's radon_partition in ~10 lines

Mathlib has radon_partition : ¬ AffineIndependent 𝕜 f → ∃ I, (convexHull (f '' I) ∩ convexHull (f '' Iᶜ)).Nonempty but not the converse. The converse is short. hf.affineSpan_disjoint_of_disjoint (disjoint_compl_right (a := I)) makes the affine spans disjoint; then .mono (convexHull_subset_affineSpan _) (convexHull_subset_affineSpan _) and Set.disjoint_iff_inter_eq_empty. That gives an iff, and with AffineBasis.exists_affineBasis_of_finiteDimensional (ι := Fin (finrank 𝕜 E + 1)) (its .ind field is the affine independence), sharpness of Radon's number d+2. Lint gotcha: these lemmas do not use [IsStrictOrderedRing 𝕜] from the section variables, so add omit [IsStrictOrderedRing 𝕜] in before the docstring.