no goals
α : Type u_1
β : Type u_2
γ : Type ?u.5624
δ : Type ?u.5627
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s
rw [hf.induced, isClosed_induced_iff]