ι : Type ?u.334826
ι' : Type ?u.334829
α : Type u_1
β : Type u_2
γ : Type ?u.334838
inst✝ : SemilatticeInf α
a : α
f : β → ↑(Iio a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
ι : Type ?u.334826
ι' : Type ?u.334829
α : Type u_1
β : Type u_2
γ : Type ?u.334838
inst✝ : SemilatticeInf α
a : α
f : β → ↑(Iio a)
l : Filter β
⊢ Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
rw [atBot_Iio_eq, tendsto_comap_iff]
no goals
ι : Type ?u.334826
ι' : Type ?u.334829
α : Type u_1
β : Type u_2
γ : Type ?u.334838
inst✝ : SemilatticeInf α
a : α
f : β → ↑(Iio a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
rfl