tendsto_logb_nhdsNE_zero_of_base_lt_one

Mathlib.Analysis.SpecialFunctions.Log.Base

URI: https://scilib.ai/kg/mathlib#Real.tendsto_logb_nhdsNE_zero_of_base_lt_one

← MathLib Explorer

English

If 0 < b < 1, then log_b(x) tends to +∞ as x tends to 0 through nonzero values.

Русский

Если 0 < b < 1, то log_b(x) стремится к +∞ при x → 0, x ≠ 0.

LaTeX

$$$0 < b < 1 \implies \lim_{x \to 0, x \neq 0} \log_b x = +\infty$$$

Lean4

theorem tendsto_logb_nhdsNE_zero_of_base_lt_one (hb₀ : 0 < b) (hb : b < 1) : Tendsto (logb b) (𝓝[≠] 0) atTop :=
  tendsto_log_nhdsNE_zero.atBot_mul_const_of_neg (inv_lt_zero.2 (log_neg hb₀ hb))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru