pow_log_le_add_one

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

For any b, x, b^{log_b x} ≤ x + 1.

Русский

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

LaTeX

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

Lean4

theorem pow_log_le_add_one (b : ℕ) : ∀ x, b ^ log b x ≤ x + 1
  | 0 => by rw [log_zero_right, Nat.pow_zero]
  | x + 1 => (pow_log_le_self b x.succ_ne_zero).trans (x + 1).le_succ

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

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

Разделы

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

Аффилиация

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