of_boundedUnder_im — Mathlib

English

If Re z tends to infinity along l and im z is bounded both above and below along l, then l is an exponential comparison filter.

Русский

Если 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\\; (\\operatorname{IsBoundedUnder}(\\ge)\\, l\\ \\operatorname{Im}) \\to\\; \\IsExpCmpFilter\\ l$$$

Lean4

theorem of_boundedUnder_im (hre : Tendsto re l atTop) (him_le : IsBoundedUnder (· ≤ ·) l im)
    (him_ge : IsBoundedUnder (· ≥ ·) l im) : IsExpCmpFilter l :=
  of_boundedUnder_abs_im hre <| isBoundedUnder_le_abs.2 ⟨him_le, him_ge⟩

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