tendsto_exp_comap_re_atTop — Mathlib

English

As the real part tends to +∞, the modulus of exp(z) tends to ∞; equivalently Tendsto exp (comap Re atTop) (cobounded ℂ).

Русский

При стремлении вещественной части к +∞ модуль exp(z) растёт без ограничений; формализация: Tendsto exp (comap Re atTop) (cobounded ℂ).

LaTeX

$$$ \operatorname{Tendsto} (\exp) (\operatorname{comap} (\operatorname{re} : \mathbb{C} \to \mathbb{R}) (\operatorname{atTop})) (\operatorname{cobounded} \mathbb{C}) $$$

Lean4

/-- `‖Complex.exp z‖ → ∞` as `Complex.re z → ∞`. -/
theorem tendsto_exp_comap_re_atTop : Tendsto exp (comap re atTop) (cobounded ℂ) :=
  comap_exp_cobounded ▸ tendsto_comap

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