∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ},
  MeasureTheory.Integrable f μ →
    0 ≤ᵐ[μ] f → ∀ {s : Set X}, (∀ x ∈ s, 1 ≤ f x) → μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)