tendsto_exp_comap_re_atBot — Mathlib

English

As the real part tends to −∞, the exponential tends to 0; Tendsto exp (comap Re atBot) (nhds 0).

Русский

При стремлении вещественной части к −∞ экспонента стремится к 0; Tendsto exp (comap Re atBot) (nhds 0).

LaTeX

$$$ \operatorname{Tendsto} \exp (\operatorname{comap}(\operatorname{re} \;\text{atBot})) (\mathcal{N}_0) $$$

Lean4

/-- `Complex.exp z → 0` as `Complex.re z → -∞`. -/
theorem tendsto_exp_comap_re_atBot : Tendsto exp (comap re atBot) (𝓝 0) :=
  comap_exp_nhds_zero ▸ tendsto_comap

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