∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} (s : ℕ → Set α) {t : Set α}, (∀ (n : ℕ), s n =ᵐ[μ] t) → Filter.liminf s Filter.atTop =ᵐ[μ] t