tendsto_comap_im_ofComplex — Mathlib

English

The map ofComplex respects the comap of the imaginary part and the atTop filter, i.e., Tendsto ofComplex through comap(im, atTop) equals Tendsto through atImInfty.

Русский

Отображение ofComplex согласуется с компапом по мнимой части и фильтру atTop: пределности эквивалентны через atImInfty.

LaTeX

$$$\text{Tendsto}(\text{ofComplex}, \text{comap}(\operatorname{im}, \text{atTop})) = \text{Tendsto} \text{atImInfty}$$$

Lean4

theorem tendsto_comap_im_ofComplex : Tendsto ofComplex (comap Complex.im atTop) atImInfty :=
  by
  simp only [atImInfty, tendsto_comap_iff, Function.comp_def]
  refine tendsto_comap.congr' ?_
  filter_upwards [preimage_mem_comap (Ioi_mem_atTop 0)] with z hz
  simp only [ofComplex_apply_of_im_pos hz, ← UpperHalfPlane.coe_im, coe_mk_subtype]

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