yn_ge_n

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

For all n, n ≤ y_n(a).

Русский

Для всех n выполняется n ≤ y_n(a).

LaTeX

$$$n \\le y^{(a)}_{n}$$$

Lean4

theorem yn_ge_n : ∀ n, n ≤ yn a1 n
  | 0 => Nat.zero_le _
  | n + 1 => show n < yn a1 (n + 1) from lt_of_le_of_lt (yn_ge_n n) (strictMono_y a1 <| Nat.lt_succ_self n)

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

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

Разделы

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

Аффилиация

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