∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : TopologicalSpace E]
  [inst_1 : ContinuousENorm E] {f : α → E},
  MeasureTheory.Integrable f μ → ∀ {ε : ENNReal}, 0 < ε → μ {x | ε < ‖f x‖ₑ} < ⊤