α : Type u_1
β : Type u_2
γ : Type ?u.34648
δ : Type ?u.34651
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (x : α) in 𝓝[s] x, p (↑(LocalHomeomorph.symm e) (↑e x))) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p x
α : Type u_1
β : Type u_2
γ : Type ?u.34648
δ : Type ?u.34651
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 (↑(LocalHomeomorph.symm e) y)) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p x
rw [e.eventually_nhdsWithin _ hx]
α : Type u_1
β : Type u_2
γ : Type ?u.34648
δ : Type ?u.34651
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
y : α
hy : ↑(LocalHomeomorph.symm e) (↑e y) = y
⊢ p (↑(LocalHomeomorph.symm e) (↑e y)) ↔ p y
α : Type u_1
β : Type u_2
γ : Type ?u.34648
δ : Type ?u.34651
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (x : α) in 𝓝[s] x, p (↑(LocalHomeomorph.symm e) (↑e x))) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p x
refine'
  eventually_congr
    ((eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy =>
      _)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.34648
δ : Type ?u.34651
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
y : α
hy : ↑(LocalHomeomorph.symm e) (↑e y) = y
⊢ p (↑(LocalHomeomorph.symm e) (↑e y)) ↔ p y
rw [hy]