Removing the local attachment holes

Every point of the compact attachment union outside the core lies in an attachment. If that point also lies in a local set C, the attachment's three-diameter enlargement is one of the holes recorded as touching C.

theorem LeanPool.Besicovitch.sdiff_iUnion_touchingBadConvexSets_subset_core {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F C : Set (EuclideanSpace ℝ (Fin 2))} {alpha : ℝ} (halpha : 0 < alpha) {chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))} (hchosen : chosen ⊆ badConvexSets mu F alpha) (hC : C ⊆ compactAttachmentUnion F chosen) : C \ ⋃ (V : ↑(touchingBadConvexSets 3 chosen C)), diameterThickening 3 ↑V ⊆ F

Removing every three-diameter enlargement which touches C leaves only points of the compact core F.