ι : Type ?u.339440
ι' : Type ?u.339443
α : Type u_1
β : Type u_2
γ : Type ?u.339452
inst✝ : SemilatticeSup α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
ι : Type ?u.339440
ι' : Type ?u.339443
α : Type u_1
β : Type u_2
γ : Type ?u.339452
inst✝ : SemilatticeSup α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f atTop l
rw [← map_val_Ici_atTop a, tendsto_map'_iff]
no goals
ι : Type ?u.339440
ι' : Type ?u.339443
α : Type u_1
β : Type u_2
γ : Type ?u.339452
inst✝ : SemilatticeSup α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
rfl