continuousOn_logb

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For fixed base b, the map x ↦ log_b x is continuous on {x ≠ 0}.

Русский

Для фиксированного основания b отображение x ↦ log_b x непрерывно на {x ≠ 0}.

LaTeX

$$$\text{ContinuousOn}(\log_b b)\; (\mathbb{R} \setminus \{0\})$$$

Lean4

theorem continuousOn_logb : ContinuousOn (logb b) {0}ᶜ :=
  continuousOn_log.div_const _

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

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

Разделы

Аффилиация

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