∀ {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (F : Set Ω) {δ : ℝ} (δ_pos : 0 < δ),
  MeasureTheory.Integrable (fun ω => ↑((thickenedIndicator δ_pos F) ω)) μ