lt_pow_of_log_lt

Mathlib.Data.Nat.Log

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

English

If log_b y < x then y < b^x.

Русский

Если log_b y < x, то y < b^x.

LaTeX

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

Lean4

theorem lt_pow_of_log_lt {b x y : ℕ} (hb : 1 < b) : log b y < x → y < b ^ x :=
  lt_imp_lt_of_le_imp_le (le_log_of_pow_le hb)

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

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

Разделы

Аффилиация

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