tendsto_mabs_atBot_atTop — Mathlib

English

In a commutative group G with linear order, the mabs function also tends to +∞ when its argument tends to -∞: as x → -∞, mabs(x) → +∞.

Русский

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

LaTeX

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

Lean4

/-- $\lim_{x\to\infty^{-1}|x|_m=+\infty$ -/
@[to_additive /-- $\lim_{x\to-\infty}|x|=+\infty$ -/
    ]
theorem tendsto_mabs_atBot_atTop [IsOrderedMonoid G] : Tendsto (mabs : G → G) atBot atTop :=
  tendsto_atTop_mono inv_le_mabs tendsto_inv_atBot_atTop

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