no goals
α : Type u_1
β : Type u_2
γ : Type ?u.64146
δ : Type ?u.64149
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set β
⊢ IsClosed (↑h ⁻¹' s) ↔ IsClosed s
simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]