no goals
α : Type u_1
β : Type u_2
γ : Type ?u.271027
δ : Type ?u.271030
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set β
hs : s ⊆ range f
⊢ IsClosed s ↔ IsClosed (f ⁻¹' s)
rw [hf.closed_iff_image_closed, image_preimage_eq_of_subset hs]