The compact union of convex attachments

If the selected holes have finite total diameter, their compact attachments accumulate only on the compact core. Consequently the core together with all attachments is compact.

def LeanPool.Besicovitch.compactAttachmentUnion (F : Set (EuclideanSpace ℝ (Fin 2))) (chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))) : Set (EuclideanSpace ℝ (Fin 2))

The compact core together with all convex pieces attached along selected holes.

Equations

• LeanPool.Besicovitch.compactAttachmentUnion F chosen = F ∪ ⋃ (V : ↑chosen), LeanPool.Besicovitch.convexAttachment F ↑V

theorem LeanPool.Besicovitch.isCompact_compactAttachmentUnion {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F : Set (EuclideanSpace ℝ (Fin 2))} (hF : IsCompact F) {alpha : ℝ} (halpha : 0 < alpha) {chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))} (hchosen : chosen ⊆ badConvexSets mu F alpha) (hsum : ∑' (V : ↑chosen), Metric.ediam ↑V ≠ ⊤) : IsCompact (compactAttachmentUnion F chosen)

Finite total hole diameter makes the full attachment union compact.