tendsto_exp_comp_nhds_zero — Mathlib

English

For any function f, exp(f(x)) → 0 along l to 0 iff f(x) → −∞ along l.

Русский

Для любой функции f, exp(f(x)) → 0 вдоль l к 0 тогда и только тогда, когда f(x) → −∞ вдоль l.

LaTeX

$$$\\displaystyle \\lim_{l} \\exp(f(x)) = 0 \\iff \\lim_{l} f(x) = -\\infty.$$$

Lean4

@[simp]
theorem tendsto_exp_comp_nhds_zero {f : α → ℝ} : Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto f l atBot := by
  simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]

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