no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p q : α → Prop
hp : IsOpen {x | p x}
hq : IsClosed {x | q x}
⊢ IsClosed {x | p x → q x}
simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq