comap_exp_nhds_zero — Mathlib

English

As the real part tends to −∞, exp(z) tends to 0; equivalently comap exp of nhds 0 equals comap re of atBot.

Русский

Пусть вещественная часть стремится к −∞, тогда exp(z) → 0; эквивалентно comap exp nhds 0 = comap re atBot.

LaTeX

$$$ \operatorname{comap} (\exp) (\mathcal{N}_0) = \operatorname{comap} (\operatorname{re}) (\operatorname{atBot}) $$$

Lean4

@[simp]
theorem comap_exp_nhds_zero : comap exp (𝓝 0) = comap re atBot :=
  calc
    comap exp (𝓝 0) = comap re (comap Real.exp (𝓝 0)) :=
      by
      rw [← comap_norm_nhds_zero, comap_comap, Function.comp_def]
      simp_rw [norm_exp, comap_comap, Function.comp_def]
    _ = comap re atBot := by rw [Real.comap_exp_nhds_zero]

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