no goals
α : Type u_1
β : Type u_2
γ : Type ?u.6389
δ : Type ?u.6392
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ Dense s ↔ ∀ (x : α), f x ∈ closure (f '' s)
simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]