∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (s s_1 : TopologicalSpace.Closeds β),
  s = s_1 → ∀ {f f_1 : α → β} (e_f : f = f_1) (hf : Continuous f), s.preimage hf = s_1.preimage ⋯