log_eq_one_iff

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

For all b and x with x ≠ 0, b^{log_b x} ≤ x.

Русский

Для всех b и x, если x ≠ 0, то b^{log_b x} ≤ x.

LaTeX

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

Lean4

theorem log_eq_one_iff {b n : ℕ} : log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n :=
  log_eq_one_iff'.trans ⟨fun h => ⟨h.2, lt_mul_self_iff.1 (h.1.trans_lt h.2), h.1⟩, fun h => ⟨h.2.2, h.1⟩⟩

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

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

Разделы

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

Аффилиация

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