no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.14588
α : Type ?u.14591
ι : Type ?u.14594
π : ι → Type ?u.14599
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
hf : Inducing f
⊢ f x ⤳ f y ↔ x ⤳ y
simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton,
  mem_preimage]