comap_exp_cobounded — Mathlib

English

The exponential map along cobounded complex space is the same as re-aligned cobounded by the real part; more precisely, comap exp of cobounded ℂ equals comap re of atTop.

Русский

Переход по экспоненте в комплексном пространстве с граничным множеством получается как comap по действительной части от atTop.

LaTeX

$$$ \operatorname{comap} (\exp) (\operatorname{cobounded} \mathbb{C}) = \operatorname{comap} (\operatorname{re}) (\operatorname{atTop}) $$$

Lean4

@[simp]
theorem comap_exp_cobounded : comap exp (cobounded ℂ) = comap re atTop :=
  calc
    comap exp (cobounded ℂ) = comap re (comap Real.exp atTop) := by
      simp only [← comap_norm_atTop, comap_comap, comp_def, norm_exp]
    _ = comap re atTop := by rw [Real.comap_exp_atTop]

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