α : Type u_1
β : Type u_2
γ : Type ?u.34147
δ : Type ?u.34150
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : β → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : β) in map (fun x => ↑e x) (𝓝[s] x), p b
α : Type u_1
β : Type u_2
γ : Type ?u.34147
δ : Type ?u.34150
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : β → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p (↑e x)
refine' Iff.trans _ eventually_map
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.34147
δ : Type ?u.34150
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : β → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : β) in map (fun x => ↑e x) (𝓝[s] x), p b
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]