α : Type u_1
β : Type ?u.8700
γ : Type ?u.8703
δ : Type ?u.8706
δ' : Type ?u.8709
ι : Sort ?u.8712
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet ((s₁ᶜ ∪ s₂ᶜ)ᶜ)
α : Type u_1
β : Type ?u.8700
γ : Type ?u.8703
δ : Type ?u.8706
δ' : Type ?u.8709
ι : Sort ?u.8712
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)
rw [inter_eq_compl_compl_union_compl]
no goals
α : Type u_1
β : Type ?u.8700
γ : Type ?u.8703
δ : Type ?u.8706
δ' : Type ?u.8709
ι : Sort ?u.8712
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet ((s₁ᶜ ∪ s₂ᶜ)ᶜ)
exact (h₁.compl.union h₂.compl).compl