log — Mathlib

English

For any real y, the limit as x → ∞ of log(x + y) − log x is 0. The difference of logs of shifted and unshifted arguments tends to zero at infinity.

Русский

Для любого вещественного y предел при x → ∞ логарифм(x + y) минус логарифм x равен 0. Разность логарифмов смещённых и несмещённых аргументов стремится к нулю на бесконечности.

LaTeX

$$$$ \\lim_{x \\to \\infty} (\\log(x+y) - \\log x) = 0. $$$$

Lean4

theorem log {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tendsto f l (𝓝 x)) (hx : x ≠ 0) :
    Tendsto (fun x => log (f x)) l (𝓝 (log x)) :=
  (continuousAt_log hx).tendsto.comp h

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