tendsto_logb_nat_add_one_sub_logb

English

For a fixed base b, the sequence log_b(k+1) − log_b(k) tends to 0 as k → ∞.

Русский

Пусть основание логарифма фиксировано. Тогда последовательность log_b(k+1) − log_b(k) стремится к 0 при k → ∞.

LaTeX

$$$\lim_{k \to \infty} \big( \log_b(k+1) - \log_b k \big) = 0$$$

Lean4

theorem tendsto_logb_nat_add_one_sub_logb : Tendsto (fun k : ℕ => logb b (k + 1) - logb b k) atTop (𝓝 0) :=
  (tendsto_logb_comp_add_sub_logb 1).comp tendsto_natCast_atTop_atTop

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