∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)} {x : ι → ℝ},
  (∀ (δ : ℝ),
      0 < δ → ∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s) →
    ¬Filter.Tendsto
        (fun r =>
          MeasureTheory.volume (closure s ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall x r))
        (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)