tendsto_deriv_mul_log_atTop — Mathlib

English

The derivative of f(x) = x log x tends to +∞ as x → ∞.

Русский

Производная функции f(x) = x log x стремится к +∞ при x → ∞.

LaTeX

$$$\lim_{x \to \infty} \frac{d}{dx}\bigl(x \log x\bigr) = \infty$$$

Lean4

theorem tendsto_deriv_mul_log_atTop : Tendsto (fun x ↦ deriv (fun x ↦ x * log x) x) atTop atTop :=
  by
  refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))
  rw [EventuallyEq, eventually_atTop]
  exact ⟨1, fun _ hx ↦ deriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

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