tendsto_neg_const_mul_pow_atTop — Mathlib

English

If c < 0 and n > 0, then c x^n tends to negative infinity as x tends to positive infinity.

Русский

Если c < 0 и n > 0, то c x^n стремится к минус бесконечности при x → +∞.

LaTeX

$$$c < 0 \land n \neq 0 \Rightarrow \operatorname{Tendsto}\left(x \mapsto c \cdot x^n, \operatorname{atTop}, \operatorname{atBot}\right)$$$

Lean4

theorem tendsto_neg_const_mul_pow_atTop {c : α} {n : ℕ} (hn : n ≠ 0) (hc : c < 0) :
    Tendsto (fun x => c * x ^ n) atTop atBot :=
  (tendsto_pow_atTop hn).const_mul_atTop_of_neg hc

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