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