α : Type u_1
β : Type ?u.910929
γ : Type ?u.910932
δ : Type ?u.910935
δ' : Type ?u.910938
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋃ (i : ℕ), ⋂ (j : ℕ) (_ : p j ∧ i ≤ j), s j)
α : Type u_1
β : Type ?u.910929
γ : Type ?u.910932
δ : Type ?u.910935
δ' : Type ?u.910938
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (bliminf s atTop p)
simp only [Filter.bliminf_eq_iSup_biInf_of_nat, iInf_eq_iInter, iSup_eq_iUnion]
no goals
α : Type u_1
β : Type ?u.910929
γ : Type ?u.910932
δ : Type ?u.910935
δ' : Type ?u.910938
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋃ (i : ℕ), ⋂ (j : ℕ) (_ : p j ∧ i ≤ j), s j)
exact .iUnion fun n => .iInter fun m => .iInter fun hm => h m hm.1