∀ {α : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  (f : BoundedContinuousFunction α ℝ) (μ : MeasureTheory.Measure α),
  0 ≤ᵐ[μ] ⇑f →
    MeasureTheory.HasFiniteIntegral (⇑f) μ → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 ‖f‖, μ.real {a | t ≤ f a}