α : Type u_1
β : Type u_2
γ : Type ?u.173393
δ : Type ?u.173396
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
h : Continuous f
⊢ f '' closure s ⊆ closure (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.173393
δ : Type ?u.173396
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
h : Continuous f
⊢ closure s ⊆ f ⁻¹' closure (f '' s)
rw [← Set.image_subset_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.173393
δ : Type ?u.173396
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
h : Continuous f
⊢ f '' closure s ⊆ closure (f '' s)
exact image_closure_subset_closure_image h