pow_pred_clog_lt_self

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

If 1 < b and 1 < x, then b^{clog_b(x) - 1} < x.

Русский

Пусть 1 < b и 1 < x. Тогда b^{clog_b(x) - 1} < x.

LaTeX

$$$ (1 < b) \\land (1 < x) \\implies b^{\\operatorname{clog}_b x - 1} < x $$$

Lean4

theorem pow_pred_clog_lt_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 1 < x) : b ^ (clog b x).pred < x :=
  by
  rw [← lt_clog_iff_pow_lt hb]
  exact pred_lt (clog_pos hb hx).ne'

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

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

Разделы

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

Аффилиация

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