atBot_pow — Mathlib

English

If f tends to −∞ along l, then for any positive natural number n, the n-th power f(x)^n tends to −∞ along l (in the dual order setting).

Русский

Если f(x) стремится к −∞ вдоль l, то для любого положительного n выражение f(x)^n стремится к −∞ вдоль l (в двойственной порядке).

LaTeX

$$$\\operatorname{Tendsto} f\\ l\\ atBot \\implies \\forall n>0, \\operatorname{Tendsto}(\\lambda x. f(x)^n)\\ l\\ atBot$$$

Lean4

@[to_additive nsmul_atBot]
theorem atBot_pow (hf : Tendsto f l atBot) {n : ℕ} (hn : 0 < n) : Tendsto (fun x => f x ^ n) l atBot :=
  Tendsto.atTop_pow (M := Mᵒᵈ) hf hn

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