strictMonoOn_natAbs

Mathlib.Data.Int.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.strictMonoOn_natAbs

English

The function natAbs is strictly increasing on the nonnegative integers.

Русский

Функция natAbs строго возрастает на неотрицательных целых числах.

LaTeX

$$$\\text{StrictMonoOn}(\operatorname{natAbs}, [0,\\infty)).$$$

Lean4

theorem strictMonoOn_natAbs : StrictMonoOn natAbs (Ici 0) := fun _ ha _ _ hab => natAbs_lt_natAbs_of_nonneg_of_lt ha hab

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

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

Разделы

Аффилиация

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