α : Type u_1
β : Type ?u.909833
γ : Type ?u.909836
δ : Type ?u.909839
δ' : Type ?u.909842
ι : 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.909833
γ : Type ?u.909836
δ : Type ?u.909839
δ' : Type ?u.909842
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (blimsup s atTop p)
simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]
no goals
α : Type u_1
β : Type ?u.909833
γ : Type ?u.909836
δ : Type ?u.909839
δ' : Type ?u.909842
ι : 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 .iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1