lt_pow_succ_log_self

Mathlib.Data.Nat.Log

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

English

For 1 < b and any x, x < b^(log_b x) + 1.

Русский

Для 1 < b и любого x: x < b^{log_b x} + 1.

LaTeX

$$$\\forall b \\in \\mathbb{N}, \\; x \\in \\mathbb{N} \\Rightarrow x < b^{\\log_b x} + 1$$$

Lean4

theorem lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) (x : ℕ) : x < b ^ (log b x).succ :=
  lt_pow_of_log_lt hb (lt_succ_self _)

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

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

Разделы

Аффилиация

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