no goals
α : Type u_1
β : Type u_2
γ : Type ?u.64614
δ : Type ?u.64617
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set α
⊢ IsClosed (↑h '' s) ↔ IsClosed s
rw [← preimage_symm, isClosed_preimage]