English
For any integer n and elements c,d, the limit of c x^n as x → Top is determined by c and n: if c = 0 or n = 0, then the limit equals d iff c = d.
Русский
Для любых n ∈ Z, c,d ∈ 𝕜 предел(c x^n) при x → ∞ определяется значениями c и n: если c = 0 или n = 0, предел равен d тогда и только тогда, когда c = d.
LaTeX
$$Tendsto (x \mapsto c x^n) atTop (\mathcal{N} d) ↔ ((c = 0) ∨ (n = 0)) ∧ c = d$$
Lean4
theorem tendsto_const_mul_zpow_atTop_nhds_iff {n : ℤ} {c d : 𝕜} (hc : c ≠ 0) :
Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0 :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
·
cases n with
| ofNat n =>
left
simpa [tendsto_const_mul_pow_nhds_iff hc] using h
| negSucc n =>
have hn := Int.negSucc_lt_zero n
exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
· rcases h with h | h
· simp only [h.left, h.right, zpow_zero, mul_one]
exact tendsto_const_nhds
· exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1
