strictMono_addNat

Mathlib.Order.Fin.Basic

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

English

For fixed m, the map x ↦ x.addNat m: Fin n → Fin (n + m) is strictly increasing.

Русский

Для фиксированного m отображение x ↦ x.addNat m: Fin(n) → Fin(n+m) строго возрастает.

LaTeX

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

Lean4

theorem strictMono_addNat (m) : StrictMono ((addNat · m) : Fin n → Fin (n + m)) := fun i j h ↦
  Nat.add_lt_add_right (show i.val < j.val from h) _

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

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

Разделы

Аффилиация

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