no goals
α : Type u_1
β : Type ?u.467
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
⊢ IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S
simp only [specializes_iff_mem_closure, IsGenericPoint, Set.ext_iff]