pow_unbounded_of_one_lt

Mathlib.Algebra.Order.Archimedean.Basic

URI: https://scilib.ai/kg/mathlib#pow_unbounded_of_one_lt

← MathLib Explorer

English

If a>1 and there is any bound b, there exists n with b < a^n.

Русский

Если a>1 и имеется граница b, существует n такое, что b < a^n.

LaTeX

$$$\\exists n:\\, \\mathbb{N},\\ b < a^{n}.$$$

Lean4

theorem pow_unbounded_of_one_lt [ExistsAddOfLE R] (x : R) (hy1 : 1 < y) : ∃ n : ℕ, x < y ^ n :=
  by
  obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hy1
  rw [add_comm]
  exact add_one_pow_unbounded_of_pos _ hz

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

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

Разделы

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

Аффилиация

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