log_le_self

Mathlib.Data.Nat.Log

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

English

For all b and x, log_b x ≤ x.

Русский

Для всех b и x верно: log_b x ≤ x.

LaTeX

$$$\\forall b, x \\in \\mathbb{N}, \\log_b x \\le x$$$

Lean4

theorem log_le_self (b x : ℕ) : log b x ≤ x :=
  if hx : x = 0 then by simp [hx] else (log_lt_self b hx).le

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

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

Разделы

Аффилиация

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