∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω NNReal),
      Filter.Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (nhds (∫⁻ (x : Ω), ↑(f x) ∂↑μ))