α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d ((s₁ \ s₂)ᶜ)
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d (s₁ \ s₂)
apply d.has_compl_iff.1
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d (s₁ᶜ ∪ s₂)
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d ((s₁ \ s₂)ᶜ)
simp [diff_eq, compl_inter]
no goals
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d (s₁ᶜ ∪ s₂)
exact d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)