LeanPool.SardMoreira.UnifDoublingCover

theorem IsUnifLocDoublingMeasure.exists_closedBall_covering_tsum_measure_le_of_measure_zero {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] {ε : ENNReal} (hε : ε ≠ 0) (f : X → Set ℝ) (s : Set X) (hμs : μ s = 0) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) : ∃ (t : Set X) (r : X → ℝ), t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ ε