∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] (μ : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X NNReal), ∫⁻ (x : X), ↑(f x) ∂μ < ⊤