∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) →
    ∀ {E : Set Ω}, μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))