tendsto_exp_atBot — Mathlib

English

The exponential function tends to 0 as the input tends to negative infinity from the right.

Русский

Функция экспоненты стремится к 0 при стремлении аргумента к минус бесконечности справа.

LaTeX

$$$\mathrm{tendsto}\,\mathrm{Real}.\exp\_{atBot} : \mathrm{Tendsto}(\exp, \mathrm{atBot}, \mathcal{N}(0)).$$$

Lean4

theorem tendsto_exp_atBot : Tendsto exp atBot (𝓝 0) :=
  (tendsto_exp_neg_atTop_nhds_zero.comp tendsto_neg_atBot_atTop).congr fun x => congr_arg exp <| neg_neg x

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