map_exp_comap_re_atTop — Mathlib

English

The image of the exponential map along the real part toward +∞ is the cobounded filter on ℂ.

Русский

Образ экспоненты при стремлении к +∞ по вещественной части даёт космобондарный фильтр на комплексной плоскости.

LaTeX

$$$\mathrm{map}\;\exp\; (\mathrm{comap}\; \mathrm{re}\; \mathrm{atTop}) = \mathrm{cobounded}\; \mathbb{C}$$$

Lean4

@[simp]
theorem map_exp_comap_re_atTop : map exp (comap re atTop) = cobounded ℂ :=
  by
  rw [← comap_exp_cobounded, map_comap, range_exp, inf_eq_left, le_principal_iff]
  exact eventually_ne_cobounded _

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