no goals
α : Type u_1
β : Type u_2
γ : Type ?u.226322
δ : Type ?u.226325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hs : ∀ (s : Set α), closure (f '' s) ⊆ f '' closure s
c : Set α
hc : IsClosed c
⊢ f '' closure c = f '' c
rw [hc.closure_eq]