α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : Disjoint s₁ s₂
⊢ Has d (⋃ (b : Bool), bif b then s₁ else s₂)
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : Disjoint s₁ s₂
⊢ Has d (s₁ ∪ s₂)
rw [union_eq_iUnion]
no goals
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : Disjoint s₁ s₂
⊢ Has d (⋃ (b : Bool), bif b then s₁ else s₂)
exact d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)