fermatNumber_strictMono

Mathlib.NumberTheory.Fermat

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

← MathLib Explorer

English

The Fermat numbers are strictly increasing: m < n implies F_m < F_n.

Русский

Числа Ферма возрастают строго: если m < n, то F_m < F_n.

LaTeX

$$$m < n \Rightarrow F_m < F_n$$$

Lean4

theorem fermatNumber_strictMono : StrictMono fermatNumber :=
  by
  intro m n
  simp only [fermatNumber, add_lt_add_iff_right, Nat.pow_lt_pow_iff_right (one_lt_two : 1 < 2), imp_self]

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

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

Разделы

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

Аффилиация

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