α : Type u_1
β : Type u_2
γ : Type ?u.195591
δ : Type ?u.195594
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ closure (f ⁻¹' s)ᶜ ⊆ (f ⁻¹' closure s)ᶜ
α : Type u_1
β : Type u_2
γ : Type ?u.195591
δ : Type ?u.195594
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ f ⁻¹' closure s ⊆ closure (f ⁻¹' s)
rw [← compl_subset_compl]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.195591
δ : Type ?u.195594
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ closure (f ⁻¹' s)ᶜ ⊆ (f ⁻¹' closure s)ᶜ
simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]