no goals
α : Type u_1
β : Type ?u.912543
γ : Type ?u.912546
δ : Type ?u.912549
δ' : Type ?u.912552
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (liminf s atTop)
simpa only [← bliminf_true] using measurableSet_bliminf fun n _ => hs n