Merging overlapping convex holes

This file replaces a countable family of possibly overlapping open holes by a countable pairwise-disjoint family of larger open convex holes. The sum of the extended diameters does not increase.

Convexifying a connected component of the original overlap graph is not sufficient: the convex hulls can acquire new intersections. We instead repeatedly merge intersecting convex hulls at each finite stage and then take the increasing union of every eventual cluster.

theorem LeanPool.Besicovitch.exists_pairwiseDisjoint_convex_hole_cover (U : ℕ → Set (EuclideanSpace ℝ (Fin 2))) (hUopen : ∀ (i : ℕ), IsOpen (U i)) (hsum : ∑' (i : ℕ), Metric.ediam (U i) ≠ ⊤) : ∃ (W : Set (Set (EuclideanSpace ℝ (Fin 2)))), W.Countable ∧ W.PairwiseDisjoint id ∧ (∀ (V : ↑W), IsOpen ↑V ∧ Convex ℝ ↑V ∧ Bornology.IsBounded ↑V) ∧ ⋃ (i : ℕ), U i ⊆ ⋃ (V : ↑W), ↑V ∧ ∑' (V : ↑W), Metric.ediam ↑V ≤ ∑' (i : ℕ), Metric.ediam (U i)

A countable family of open holes with finite total diameter has a pairwise-disjoint open convex enlargement without any increase in total diameter.