ι : Type ?u.53584
ι' : Type ?u.53587
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x => ↑e (f x)) l atTop ↔ Tendsto (↑e ∘ f) l atTop
ι : Type ?u.53584
ι' : Type ?u.53587
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x => ↑e (f x)) l atTop ↔ Tendsto f l atTop
rw [← e.comap_atTop, tendsto_comap_iff]
no goals
ι : Type ?u.53584
ι' : Type ?u.53587
α : Type u_2
β : Type u_3
γ : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x => ↑e (f x)) l atTop ↔ Tendsto (↑e ∘ f) l atTop
rfl