tendsto_comp_exp_atBot — Mathlib

English

For any f, Tendsto (f( exp x)) atBot l iff Tendsto f (nhdsWithin 0 (Ioi 0)) l.

Русский

Для произвольной f, Tendsto (f( exp x)) при atBot эквивалентно Tendsto f в nhdsWithin 0(Ioi 0).

LaTeX

$$$\\operatorname{Tendsto}(f \\circ \\exp)\\;\\text{atBot}\\;l \\iff \\operatorname{Tendsto} f\\;\\mathcal{N}_{(0,\\infty)}\\;l.$$$

Lean4

theorem tendsto_comp_exp_atBot {f : ℝ → α} : Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l :=
  by
  rw [← map_exp_atBot, tendsto_map'_iff]
  rfl

Похожие утверждения