pred

Mathlib.Data.Num.Basic

URI: https://scilib.ai/kg/mathlib#PosNum.pred

Lean4

/-- The predecessor of a `PosNum` as a `PosNum`. This means that `pred 1 = 1`. -/
def pred (a : PosNum) : PosNum :=
  Num.casesOn (pred' a) 1 id

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

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

Разделы

Аффилиация

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