ι : Type ?u.335766
ι' : Type ?u.335769
α : Type u_1
β : Type u_2
γ : Type ?u.335778
inst✝ : SemilatticeSup α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
ι : Type ?u.335766
ι' : Type ?u.335769
α : Type u_1
β : Type u_2
γ : Type ?u.335778
inst✝ : SemilatticeSup α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
rw [atTop_Ici_eq, tendsto_comap_iff]
no goals
ι : Type ?u.335766
ι' : Type ?u.335769
α : Type u_1
β : Type u_2
γ : Type ?u.335778
inst✝ : SemilatticeSup α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
rfl