tendsto_exp_comap_re_atBot_nhdsNE

English

Along comap Re atBot excluding 0, exp(z) tends to 0; i.e., Tendsto exp (comap Re atBot) (nhds[≠] 0).

Русский

Вдоль comap Re atBot, исключая 0, exp(z) стремится к 0; Tendsto exp (comap Re atBot) (nhds[≠] 0).

LaTeX

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

Lean4

theorem tendsto_exp_comap_re_atBot_nhdsNE : Tendsto exp (comap re atBot) (𝓝[≠] 0) :=
  comap_exp_nhdsNE ▸ tendsto_comap

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