not_tendsto_pow_atTop_atBot — Mathlib

English

For every natural n, the map x ↦ x^n does not tend to both infinities as x grows without bound; in particular Tendsto (x^n) atTop atBot is false for all n.

Русский

Для каждого натурального n функция x ↦ x^n не стремится одновременно к верхнему и к нижнему пределу при x→∞; в частности для любого n не выполняется Tendsto (x^n) приTop приBot.

LaTeX

$$$$\forall n \in \mathbb{N},\; \neg \lim_{x \to \infty} x^n = -\infty.$$$$

Lean4

theorem not_tendsto_pow_atTop_atBot [Ring α] [LinearOrder α] [IsStrictOrderedRing α] :
    ∀ {n : ℕ}, ¬Tendsto (fun x : α => x ^ n) atTop atBot
  | 0 => by simp [not_tendsto_const_atBot]
  | n + 1 => (tendsto_pow_atTop n.succ_ne_zero).not_tendsto disjoint_atTop_atBot

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