tendsto_mabs_atTop_atTop — Mathlib

English

In a commutative group G with a linear order, the multiplicative absolute-value function mabs grows without bound along the positive direction: as x tends to +∞, mabs(x) tends to +∞.

Русский

В коммутативной группе G с линейным порядком функция м ABS(x) растет до бесконечности: при возрастании x к +∞, mabs(x) стремится к +∞.

LaTeX

$$$\\operatorname{Tendsto}(\\mathrm{mabs}: G \\to G)\\; \\operatorname{atTop} \\; \\operatorname{atTop}$$$

Lean4

/-- $\lim_{x\to+\infty}|x|_m=+\infty$ -/
@[to_additive /-- $\lim_{x\to+\infty}|x|=+\infty$ -/
    ]
theorem tendsto_mabs_atTop_atTop : Tendsto (mabs : G → G) atTop atTop :=
  tendsto_atTop_mono le_mabs_self tendsto_id

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