no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
p : α → Prop
⊢ (∃ t, t ⊆ {x | (fun x => p x) x} ∧ IsOpen t ∧ a ∈ t) ↔ ∃ t, (∀ (x : α), x ∈ t → p x) ∧ IsOpen t ∧ a ∈ t
simp only [subset_def, exists_prop, mem_setOf_eq]