no goals
α : Type u_1
β : Type u_2
γ : Type ?u.196325
δ : Type ?u.196328
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)
simpa only [frontier_eq_closure_inter_closure, preimage_inter] using
  inter_subset_inter hf.preimage_closure_subset_closure_preimage
    hf.preimage_closure_subset_closure_preimage