no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
t : Set α
⊢ (∃ x, (a ∈ xᶜ ∧ IsOpen (xᶜ)) ∧ xᶜ ⊆ t) ↔ ∃ i, (¬a ∈ i ∧ IsClosed i) ∧ iᶜ ⊆ t
simp only [isOpen_compl_iff, mem_compl_iff]