α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto (f ∘ exp) atBot l
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto f (𝓝[Set.Ioi 0] 0) l
rw [← map_exp_atBot, tendsto_map'_iff]
no goals
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto (f ∘ exp) atBot l
rfl