map_exp_comap_re_atBot — Mathlib

English

The image of the exponential map along the real part toward −∞ is the punctured neighborhood of 0; i.e., exp sends approaching −∞ in the real part to points near 0 but never 0.

Русский

Пусть идёт следование к минус бесконечности по действительной части; экспонента приближает ноль, но не достигает него.

LaTeX

$$$\mathrm{map}\;\exp\; (\mathrm{comap}\; \mathrm{re}\; \mathrm{atBot}) = (\mathcal{N}_{0})^{\setminus {0}}$$$

Lean4

@[simp]
theorem map_exp_comap_re_atBot : map exp (comap re atBot) = 𝓝[≠] 0 := by
  rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]

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