α : Type u_1
β : Type u_2
γ : Type ?u.175018
δ : Type ?u.175021
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type ?u.175033
ι : Type ?u.175036
f✝ : κ → β
g : β → γ
f : α → β
hf : Continuous f
s : Set α
hs : Dense s
⊢ f '' closure s ⊆ closure (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.175018
δ : Type ?u.175021
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type ?u.175033
ι : Type ?u.175036
f✝ : κ → β
g : β → γ
f : α → β
hf : Continuous f
s : Set α
hs : Dense s
⊢ range f ⊆ closure (f '' s)
rw [← image_univ, ← hs.closure_eq]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.175018
δ : Type ?u.175021
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type ?u.175033
ι : Type ?u.175036
f✝ : κ → β
g : β → γ
f : α → β
hf : Continuous f
s : Set α
hs : Dense s
⊢ f '' closure s ⊆ closure (f '' s)
exact image_closure_subset_closure_image hf