no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44868
δ : Type ?u.44871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x✝ : α
y : β
h : IsImage e s t
x : α
hx : x ∈ e.source
⊢ ↑e x ∈ closure t ↔ x ∈ closure s
simp only [mem_closure_iff_nhdsWithin_neBot, ← h.map_nhdsWithin_eq hx, map_neBot_iff]