tendsto_abs_re — Mathlib

English

If l is an exponential comparison filter, then |z.re| tends to infinity along l.

Русский

Если l — экспоненциальный сравнительный фильтр, то по модулю |Re z| стремится к бесконечности вдоль l.

LaTeX

$$$\\forall l:\\,\\mathsf{IsExpCmpFilter}\\ l \\Rightarrow \\operatorname{Tendsto} (\\lambda z: |z.re|)\\ l\\ \\operatorname{atTop}$$$

Lean4

theorem tendsto_abs_re (hl : IsExpCmpFilter l) : Tendsto (fun z : ℂ => |z.re|) l atTop :=
  tendsto_abs_atTop_atTop.comp hl.tendsto_re

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