tendsto_logb_nhdsGT_zero_of_base_lt_one

English

For b not equal to −1,0,1, the function x ↦ |log_b x| tends to +∞ as x → +∞.

Русский

Для b ∉ {−1,0,1} функция x ↦ |log_b x| стремится к +∞ при x → +∞.

LaTeX

$$$b \neq -1,0,1 \Rightarrow \lim_{x \to \infty} |\log_b x| = \infty$$$

Lean4

theorem tendsto_logb_nhdsGT_zero_of_base_lt_one (hb₀ : 0 < b) (hb : b < 1) : Tendsto (logb b) (𝓝[>] 0) atTop :=
  tendsto_log_nhdsGT_zero.atBot_mul_const_of_neg (inv_lt_zero.2 (log_neg hb₀ hb))

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