α : Type u_1
β : Type ?u.8432
γ : Type ?u.8435
δ : Type ?u.8438
δ' : Type ?u.8441
ι : Sort ?u.8444
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ (b : Bool), bif b then s₁ else s₂)
α : Type u_1
β : Type ?u.8432
γ : Type ?u.8435
δ : Type ?u.8438
δ' : Type ?u.8441
ι : Sort ?u.8444
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∪ s₂)
rw [union_eq_iUnion]
no goals
α : Type u_1
β : Type ?u.8432
γ : Type ?u.8435
δ : Type ?u.8438
δ' : Type ?u.8441
ι : Sort ?u.8444
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ (b : Bool), bif b then s₁ else s₂)
exact .iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)