no goals
α : Type u_1
β : Type u_2
γ : Type ?u.136882
δ : Type ?u.136885
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]