∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {f : ι → α → β},
        (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
          (∀ (ε : ℝ),
              0 < ε →
                ∃ C,
                  0 < C ∧
                    ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
            MeasureTheory.UnifIntegrable f p μ