tendsto_pow_atTop_atTop_of_one_lt

English

For 𝕜 a field with appropriate topology, the sequence r^n tends to 0 as n→∞ if and only if |r|<1.

Русский

Для поля 𝕜 при соответствующей топологии, последовательность r^n сходится к 0 тогда и только тогда, когда |r|<1.

LaTeX

$$$$ \\lim_{n\\to\\infty} r^n = 0 \\quad\\text{iff } |r| < 1.$$$$

Lean4

theorem tendsto_pow_atTop_atTop_of_one_lt [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α}
    (h : 1 < r) : Tendsto (fun n : ℕ ↦ r ^ n) atTop atTop :=
  sub_add_cancel r 1 ▸ tendsto_add_one_pow_atTop_atTop_of_pos (sub_pos.2 h)

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