strictMonoOn_logb

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

The function log_b is strictly monotone on the positive reals: if 0 < x < y then log_b x < log_b y.

Русский

Функция log_b строго возрастает на положительных числах: если 0 < x < y, то log_b x < log_b y.

LaTeX

$$$1 < b \Rightarrow \text{StrictMonoOn}(\log_b, \mathbb{R}_{>0}).$$$

Lean4

theorem strictMonoOn_logb : StrictMonoOn (logb b) (Set.Ioi 0) := fun _ hx _ _ hxy => logb_lt_logb hb hx hxy

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

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

Разделы

Аффилиация

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