Maximal disjoint selection

This file extracts a countable disjoint subfamily of uniformly bounded open sets. Every original set meets a selected set whose diameter is more than half as large.

theorem LeanPool.Besicovitch.exists_countable_disjoint_subfamily (family : Set (Set (EuclideanSpace ℝ (Fin 2)))) (hopen : ∀ V ∈ family, IsOpen V) (hnonempty : ∀ V ∈ family, V.Nonempty) (hbounded : ∀ V ∈ family, Bornology.IsBounded V) (R : ℝ) (hdiam : ∀ V ∈ family, Metric.diam V ≤ R) : ∃ chosen ⊆ family, chosen.PairwiseDisjoint id ∧ chosen.Countable ∧ ∀ V ∈ family, ∃ W ∈ chosen, (V ∩ W).Nonempty ∧ Metric.diam V < 2 * Metric.diam W

A uniformly bounded family of nonempty bounded open sets has a countable disjoint subfamily meeting every member at a scale larger than half its diameter.