α : Type u_1
β : Type u_2
γ : Type ?u.7316
δ : Type ?u.7319
δ' : Type ?u.7322
ι : Sort ?u.7325
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (i : β) (_ : i ∈ s), f iᶜ)
α : Type u_1
β : Type u_2
γ : Type ?u.7316
δ : Type ?u.7319
δ' : Type ?u.7322
ι : Sort ?u.7325
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet ((⋂ (b : β) (_ : b ∈ s), f b)ᶜ)
rw [compl_iInter₂]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.7316
δ : Type ?u.7319
δ' : Type ?u.7322
ι : Sort ?u.7325
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (i : β) (_ : i ∈ s), f iᶜ)
exact .biUnion hs fun b hb => (h b hb).compl