{Ω : Type u_1} →
  {ι : Type u_2} →
    {E : Type u_3} →
      {m : MeasurableSpace Ω} →
        {mE : MeasurableSpace E} →
          [inst : TopologicalSpace E] →
            [OpensMeasurableSpace E] →
              (ι → Ω → E) →
                Filter ι →
                  (Ω → E) →
                    (μ : autoParam (MeasureTheory.Measure Ω) MeasureTheory.TendstoInDistribution._auto_1) →
                      [MeasureTheory.IsProbabilityMeasure μ] → Prop