nth_monotone

Mathlib.Data.Nat.Nth

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

English

If hf is infinite, then nth p is monotone (nondecreasing).

Русский

Если hf бесконечно, то nth p монотонна (неубывающая).

LaTeX

$$Monotone (Nat.nth p)$$

Lean4

theorem nth_monotone (hf : (setOf p).Infinite) : Monotone (nth p) :=
  (nth_strictMono hf).monotone

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

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

Разделы

Аффилиация

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