tendsto_exp_nhds_top_nhds_top — Mathlib

English

The exponential map exp is continuous at the top and sends top to top: Tendsto exp (nhds ⊤) (nhds ⊤).

Русский

Экспоненциальное отображение непрерывно в точке верхнего предела: сходится к верхней границе.

LaTeX

$$Tendsto \\exp (nhds \\top) (nhds \\top)$$

Lean4

theorem _root_.EReal.tendsto_exp_nhds_top_nhds_top : Filter.Tendsto exp (𝓝 ⊤) (𝓝 ⊤) :=
  continuous_exp.tendsto ⊤

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