Blaschke selection + isodiametric inequality in Lean/Mathlib: what is already there

Mathlib (v4.35) already has most of Blaschke selection: NonemptyCompacts E is a MetricSpace with dist_eq : dist C D = hausdorffDist C D, it is a CompleteSpace when E is, and NonemptyCompacts.totallyBounded_subsets_of_totallyBounded (in Topology/UniformSpace/Closeds.lean) gives total boundedness of {C | C ⊆ t}. Missing: convexity is closed. Prove it with isClosed_of_closure_subset + Metric.mem_closure_iff twice (once in NonemptyCompacts, once for the point a•x+b•y in C, closed since compact), and exists_dist_lt_of_hausdorffDist_lt (finiteness side goal: hausdorffEDist_ne_top_of_nonempty_of_bounded). Bound dist (a•x+b•y) (a•x'+b•y') by a*m + b*m = m with m = max of the two distances; avoids case splits on a = 0. Compactness: (totallyBounded ...).isCompact_of_isClosed (the name is TotallyBounded.isCompact_of_isClosed, not isCompact_of_totallyBounded_isClosed). Then IsCompact.tendsto_subseq gives the subsequence. Isodiametric inequality μ A ≤ μ(closedBall 0 (diam A / 2)) for any norm: Brunn-Minkowski 2^n μ A ≤ μ(A - A), A - A ⊆ closedBall 0 (diam A) via dist_le_diam_of_mem, and Measure.addHaar_closedBall_mul μ 0 (r := 2) to pull out 2^n; cancel with ENNReal.mul_le_mul_iff_right. Non-measurable A: pass to closure, diam of closure via simp only [diam, ediam_closure].