log_lt_self

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

For any base b and nonzero x, log_b x < x.

Русский

Для любого основания b и ненулевого x: log_b x < x.

LaTeX

$$$\\forall b, x \\in \\mathbb{N}, \\; x \\neq 0 \\Rightarrow \\log_b x < x$$$

Lean4

theorem log_lt_self (b : ℕ) {x : ℕ} (hx : x ≠ 0) : log b x < x :=
  match le_or_gt b 1 with
  | .inl h => log_of_left_le_one h x ▸ Nat.pos_iff_ne_zero.2 hx
  | .inr h => log_lt_of_lt_pow hx <| Nat.lt_pow_self h

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

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

Разделы

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

Аффилиация

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