tendsto_logb_comp_add_sub_logb — Mathlib

English

For a fixed base b and any real y, as x → ∞, log_b(x+y) − log_b x → 0.

Русский

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

LaTeX

$$$\lim_{x \to \infty} \big( \log_b(x+y) - \log_b x \big) = 0$$$

Lean4

theorem tendsto_logb_comp_add_sub_logb (y : ℝ) : Tendsto (fun x : ℝ => logb b (x + y) - logb b x) atTop (𝓝 0) := by
  simpa [sub_div] using (tendsto_log_comp_add_sub_log y).div_const (log b)

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