zero

Mathlib.Data.Fin.Fin2

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

English

Zero is less than every successor: IsLT 0 (succ n) for all n.

Русский

0 меньше любого следующего числа: 0 < n+1 для всех n.

LaTeX

$$$\forall n,\ IsLT\ 0\ (\mathrm{succ}\ n)$$$

Lean4

instance zero (n) : IsLT 0 (succ n) :=
  ⟨succ_pos _⟩

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

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

Разделы

Аффилиация

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