clog_mono

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

If hc: 1 < c, hb: c ≤ b, hm n ≤ m, then clog_b m ≤ clog_c n.

Русский

Если 1 < c, c ≤ b и m ≤ n, то clog_b m ≤ clog_c n.

LaTeX

$$$ (1 < c) \\land (c \\le b) \\land (m \\le n) \\implies \\operatorname{clog}_b m \\le \\operatorname{clog}_c n $$$

Lean4

@[mono, gcongr]
theorem clog_mono {b c m n : ℕ} (hc : 1 < c) (hb : c ≤ b) (hmn : m ≤ n) : clog b m ≤ clog c n :=
  (clog_anti_left hc hb).trans <| by gcongr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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