∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure X}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (f : BoundedContinuousFunction X ℝ), 0 ≤ f → Filter.limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ) →
    ∀ (f : BoundedContinuousFunction X ℝ), Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (nhds (∫ (x : X), f x ∂μ))