clog_antitone_left

Mathlib.Data.Nat.Log

URI: https://scilib.ai/kg/mathlib#Nat.clog_antitone_left

English

For each n, the function b ↦ clog_b(n) is antitone on the set {b > 1}.

Русский

Для каждого n функция b ↦ clog_b(n) на множестве {b > 1} антимонотонна.

LaTeX

$$$ \\text{AntitoneOn}(\\lambda b, \\operatorname{clog}_b n, \\mathrm{SetIoi}(1)) $$$

Lean4

theorem clog_antitone_left {n : ℕ} : AntitoneOn (fun b : ℕ => clog b n) (Set.Ioi 1) := fun _ hc _ _ hb =>
  clog_anti_left (Set.mem_Iio.1 hc) hb

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

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

Разделы

Аффилиация

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