tendsto_coe_atImInfty — Mathlib

English

The inclusion map from the upper half-plane to the complex plane is continuous when approaching ImInfty along the atImInfty filter, i.e., Tendsto(coe, atImInfty, comap im atTop).

Русский

Включение из верхней полуплоскости в комплекс непрерывно при стремлении к бесконечности вдоль фильтра atImInfty; то есть Tendsto(coe, atImInfty, comap im atTop).

LaTeX

$$$\text{Tendsto}(\text{UpperHalfPlane.coe}, \text{atImInfty}, \text{comap}(\operatorname{im}, \text{atTop}))$$$

Lean4

theorem tendsto_coe_atImInfty : Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop) := by
  simpa only [atImInfty, tendsto_comap_iff, Function.comp_def, funext UpperHalfPlane.coe_im] using tendsto_comap

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