ι : Type ?u.341777
ι' : Type ?u.341780
α : Type u_1
β : Type u_2
γ : Type ?u.341789
inst✝ : SemilatticeInf α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l
ι : Type ?u.341777
ι' : Type ?u.341780
α : Type u_1
β : Type u_2
γ : Type ?u.341789
inst✝ : SemilatticeInf α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f atBot l
rw [← map_val_Iic_atBot a, tendsto_map'_iff]
no goals
ι : Type ?u.341777
ι' : Type ?u.341780
α : Type u_1
β : Type u_2
γ : Type ?u.341789
inst✝ : SemilatticeInf α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l
rfl