∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ →
    Filter.Tendsto (fun A => ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ) Filter.atTop (nhds (∫ (x : α), f x ∂μ))