atTop_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.

Русский

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

LaTeX

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

Lean4

@[to_additive nsmul_atTop]
theorem atTop_pow (hf : Tendsto f l atTop) {n : ℕ} (hn : 0 < n) : Tendsto (fun x => f x ^ n) l atTop :=
  by
  refine tendsto_atTop_mono' _ ((hf.eventually_ge_atTop 1).mono fun x hx ↦ ?_) hf
  simpa only [pow_one] using pow_le_pow_right' hx hn

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