tendsto_logb_atTop

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For base b > 1, log_b(x) tends to +∞ as x → +∞.

Русский

Для основания b > 1, log_b(x) растет до +∞, когда x → +∞.

LaTeX

$$$b>1 \Rightarrow \lim_{x\to\infty} \log_b x = \infty$$$

Lean4

theorem tendsto_logb_atTop : Tendsto (logb b) atTop atTop :=
  Tendsto.atTop_div_const (log_pos hb) tendsto_log_atTop

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

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

Разделы

Аффилиация

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