no goals
α : Type u_1
β : Type u_2
γ : Type ?u.170252
δ : Type ?u.170255
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ (∀ (x : Set β), IsOpen (xᶜ) → IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set β), IsClosed s → IsClosed (f ⁻¹' s)
simp only [isOpen_compl_iff, preimage_compl]