log_eq_one_iff'

Mathlib.Data.Nat.Log

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

English

For 1 < b, if b^x ≤ y then x ≤ log_b y.

Русский

Для 1 < b, если b^x ≤ y, то x ≤ log_b y.

LaTeX

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

Lean4

theorem log_eq_one_iff' {b n : ℕ} : log b n = 1 ↔ b ≤ n ∧ n < b * b := by
  rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]

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

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

Разделы

Аффилиация

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