α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen (s₁ᶜ)
h₂ : IsOpen (s₂ᶜ)
⊢ IsOpen ((s₁ ∩ s₂)ᶜ)
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsClosed s₁
h₂ : IsClosed s₂
⊢ IsClosed (s₁ ∩ s₂)
rw [← isOpen_compl_iff] at *
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen (s₁ᶜ)
h₂ : IsOpen (s₂ᶜ)
⊢ IsOpen (s₁ᶜ ∪ s₂ᶜ)
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen (s₁ᶜ)
h₂ : IsOpen (s₂ᶜ)
⊢ IsOpen ((s₁ ∩ s₂)ᶜ)
rw [compl_inter]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen (s₁ᶜ)
h₂ : IsOpen (s₂ᶜ)
⊢ IsOpen (s₁ᶜ ∪ s₂ᶜ)
exact IsOpen.union h₁ h₂