tendsto_add_one_pow_atTop_atTop_of_pos

English

If r>1, then r^n → ∞ as n → ∞.

Русский

Если r>1, то r^n растёт без границ при n→∞.

LaTeX

$$$$ \\lim_{n\\to\\infty} r^n = \\infty \\quad (r>1). $$$$

Lean4

theorem tendsto_add_one_pow_atTop_atTop_of_pos [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α]
    {r : α} (h : 0 < r) : Tendsto (fun n : ℕ ↦ (r + 1) ^ n) atTop atTop :=
  tendsto_atTop_atTop_of_monotone' (pow_right_mono₀ <| le_add_of_nonneg_left h.le) <|
    not_bddAbove_iff.2 fun _ ↦ Set.exists_range_iff.2 <| add_one_pow_unbounded_of_pos _ h

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