succ

Mathlib.Data.Fin.Fin2

URI: https://scilib.ai/kg/mathlib#Fin2.IsLT.succ

English

IsLT m n implies IsLT (succ m) (succ n): order is preserved by successor.

Русский

Если m < n, то m+1 < n+1.

LaTeX

$$$\forall m\ n,\ (l : IsLT m n),\ IsLT (succ\ m) (succ\ n)$$$

Lean4

instance succ (m n) [l : IsLT m n] : IsLT (succ m) (succ n) :=
  ⟨succ_lt_succ l.h⟩

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

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

Разделы

Аффилиация

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