tendsto_norm — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall l:\\,\\mathsf{IsExpCmpFilter}\\ l \\Rightarrow \\operatorname{Tendsto} \\|z\\|\\ l\\ \\operatorname{atTop}$$$

Lean4

theorem tendsto_norm (hl : IsExpCmpFilter l) : Tendsto norm l atTop :=
  tendsto_atTop_mono abs_re_le_norm hl.tendsto_abs_re

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