xn_ge_a_pow

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

For all a with a > 1 and n, a^n ≤ x_n(a1,n).

Русский

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

LaTeX

$$$ a^n \le x_n(a1, n) $$$

Lean4

theorem xn_ge_a_pow : ∀ n : ℕ, a ^ n ≤ xn a1 n
  | 0 => le_refl 1
  | n + 1 => by
    simp only [_root_.pow_succ, xn_succ]
    exact le_trans (Nat.mul_le_mul_right _ (xn_ge_a_pow n)) (Nat.le_add_right _ _)

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

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

Разделы

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

Аффилиация

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