of_boundedUnder_abs_im — Mathlib

English

Let l be a filter with Re z → +∞ along l and |Im z| bounded along l. Then l is an exponential comparison filter.

Русский

Пусть l — фильтр, для которого Re z → ∞ вдоль l и |Im z| ограничено вдоль l. Тогда l — экспоненциальный сравнительный фильтр.

LaTeX

$$$\\forall l:\\,\\mathsf{Filter}\\,\\mathbb{C},\\; \\operatorname{Tendsto} (\\operatorname{re})\\, l\\, \\operatorname{atTop} \\;\\to\\; \\operatorname{IsBoundedUnder}(\\le)\\, l\\ \\operatorname{Im} \\;\\to\\; \\IsExpCmpFilter\\ l$$$

Lean4

theorem of_boundedUnder_abs_im (hre : Tendsto re l atTop) (him : IsBoundedUnder (· ≤ ·) l fun z => |z.im|) :
    IsExpCmpFilter l :=
  of_isBigO_im_re_pow hre 0 <| by simpa only [pow_zero] using him.isBigO_const (f := im) one_ne_zero

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