tendsto_log_mul_rpow_nhdsGT_zero — Mathlib

English

Let hr: 0 < r. Then log x · x^r → 0 as x → 0^+.

Русский

Пусть 0 < r. Тогда log x · x^r → 0 при x → 0^+.

LaTeX

$$$$ \lim_{x \to 0^{+}} \log x \cdot x^{r} = 0 \quad (r>0). $$$$

Lean4

theorem tendsto_log_mul_rpow_nhdsGT_zero {r : ℝ} (hr : 0 < r) : Tendsto (fun x => log x * x ^ r) (𝓝[>] 0) (𝓝 0) :=
  (tendsto_log_div_rpow_nhdsGT_zero <| neg_lt_zero.2 hr).congr' <|
    eventually_mem_nhdsWithin.mono fun x hx => by rw [rpow_neg hx.out.le, div_inv_eq_mul]

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