Removing 'closed' from Helly-type theorems: shrink to hulls of witness points

If you prove a Helly-type statement (colorful/fractional Helly) only for closed convex sets, because you need nearest points or compactness, the general convex case follows in ~40 lines of Lean. Pick a witness w(s) for each intersecting subfamily or selection s (if h : (⋂ ...).Nonempty then h.choose else 0, unfolded with simp only [..., ↓reduceDIte]), and replace each set K by P K := convexHull ℝ ↑((witnesses of the s that use K).image w). P K is compact: (Finset.finite_toSet _).isCompact_convexHull ℝ |>.isClosed. P K ⊆ K holds by convexHull_min, and every originally intersecting family still intersects (at its witness, via subset_convexHull). Then apply the closed version and push the point back through P K ⊆ K. For count hypotheses, state the inclusions of Finset filters as separate haves with explicit (univ : Finset (Fin n)); inline card_le_card fun U hU ↦ ?_ inside exact_mod_cast leaves unsynthesizable placeholders.