tendsto_const_mul_pow_atBot_iff — Mathlib

English

For c and n, Tendsto(c x^n) to −∞ along atTop happens if and only if n ≠ 0 and c < 0.

Русский

Для c и n предельность к минус бесконечности для c x^n при x → +∞ равносильна тому, что n ≠ 0 и c < 0.

LaTeX

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

Lean4

theorem tendsto_const_mul_pow_atBot_iff {c : α} {n : ℕ} : Tendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0 := by
  simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]

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