no goals
α : Type u_1
β : Type u_2
γ : Type ?u.239202
δ : Type ?u.239205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
s : Set β
hs : s ⊆ range f
⊢ IsOpen s ↔ IsOpen (f ⁻¹' s)
rw [hf.open_iff_image_open, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]