tendsto_const_mul_pow_atTop — Mathlib

English

For any positive integer exponent n, the map x ↦ x^n tends to infinity as x tends to infinity in a linearly ordered semifield.

Русский

Для любого положительного целочисленного показателя n, отображение x ↦ x^n стремится к бесконечности, когда x → ∞ в линейно упорядоченном полуполе.

LaTeX

$$$\forall n \in \mathbb{Z},\; n>0 \Rightarrow \operatorname{Tendsto}(x \mapsto x^{n})\operatorname{atTop}\operatorname{atTop}$$$

Lean4

theorem tendsto_const_mul_pow_atTop (hn : n ≠ 0) (hc : 0 < c) : Tendsto (fun x => c * x ^ n) atTop atTop :=
  Tendsto.const_mul_atTop hc (tendsto_pow_atTop hn)

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