α : Type u_1
β : Type u_2
γ : Type ?u.172565
δ : Type ?u.172568
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
hc : Continuous f
⊢ ∀ ⦃x : α⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)
α : Type u_1
β : Type u_2
γ : Type ?u.172565
δ : Type ?u.172568
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
hc : Continuous f
⊢ MapsTo f (closure s) (closure t)
simp only [MapsTo, mem_closure_iff_clusterPt]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.172565
δ : Type ?u.172568
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
hc : Continuous f
⊢ ∀ ⦃x : α⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)
exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)