tendsto_exp_nhds_zero_iff — Mathlib

English

For any f, exp(f) tends to 0 along l if and only if f tends to −∞ along l.

Русский

Для любой f, exp(f) стремится к 0 вдоль l тогда и только тогда, когда f стремится к −∞ вдоль l.

LaTeX

$$$ \operatorname{Tendsto} (\exp \circ f) l (\mathcal{N}_0) \iff \operatorname{Tendsto} f l (\operatorname{atBot}) $$$

Lean4

theorem tendsto_exp_nhds_zero_iff {α : Type*} {l : Filter α} {f : α → ℂ} :
    Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto (fun x => re (f x)) l atBot :=
  by
  simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]
  rfl

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