n_lt_xn

Mathlib.NumberTheory.PellMatiyasevic

URI: https://scilib.ai/kg/mathlib#Pell.n_lt_xn

English

For all a > 1 and n, n < x_n(a1,n).

Русский

Для всех a > 1 и n выполняется n < x_n(a1,n).

LaTeX

$$$ n < x_n(a1, n) $$$

Lean4

theorem n_lt_xn (n) : n < xn a1 n :=
  lt_of_lt_of_le (Nat.lt_pow_self a1) (xn_ge_a_pow a1 n)

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

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

Разделы

Аффилиация

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