appr_mono

Mathlib.NumberTheory.Padics.RingHoms

URI: https://scilib.ai/kg/mathlib#PadicInt.appr_mono

← MathLib Explorer

English

For a fixed x in ℤ_p, the sequence n ↦ appr(x,n) is nondecreasing.

Русский

Для данного x ∈ ℤ_p последовательность n ↦ appr(x,n) неубывающая.

LaTeX

$$Monotone(n ↦ \operatorname{appr}(x,n)).$$

Lean4

theorem appr_mono (x : ℤ_[p]) : Monotone x.appr :=
  by
  apply monotone_nat_of_le_succ
  intro n
  dsimp [appr]
  split_ifs; · rfl
  apply Nat.le_add_right

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

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

Разделы

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

Аффилиация

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