tendsto_logb_nhdsNE_zero

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

If the base b > 1, then log_b(x) tends to −∞ as x tends to 0 through nonzero values.

Русский

Если основание b > 1, то log_b(x) стремится к −∞ при x → 0, x ≠ 0.

LaTeX

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

Lean4

theorem tendsto_logb_nhdsNE_zero (hb : 1 < b) : Tendsto (logb b) (𝓝[≠] 0) atBot :=
  tendsto_log_nhdsNE_zero.atBot_div_const (log_pos hb)

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

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

Разделы

Аффилиация

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