no goals
X : Type u_1
Y : Type ?u.31356
Z : Type ?u.31359
α : Type ?u.31362
ι : Type ?u.31365
π : ι → Type ?u.31370
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
⊢ x ⤳ y ∧ y ⤳ x ↔ x ∈ closure {y} ∧ y ∈ closure {x}
simp only [specializes_iff_mem_closure, and_comm]