∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → ∀ {s : Set Y}, s ⊆ Set.range f → (IsClosed s ↔ IsClosed (f ⁻¹' s))