strictMono_natAdd

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.strictMono_natAdd

English

For every n, the map natAdd n: Fin m → Fin (n + m) is strictly increasing.

Русский

Для любого n отображение natAdd n: Fin(m) → Fin(n+m) строго возрастает.

LaTeX

$$$\forall i,j:\mathrm{Fin}(m), i

Lean4

theorem strictMono_natAdd (n) : StrictMono (natAdd n : Fin m → Fin (n + m)) := fun i j h ↦
  Nat.add_lt_add_left (show i.val < j.val from h) _

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

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

Разделы

Аффилиация

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