ppred

Mathlib.Data.Nat.PSub

URI: https://scilib.ai/kg/mathlib#Nat.ppred

← MathLib Explorer

English

ppred is a partial predecessor: ppred 0 = none, ppred(n+1) = some n.

Русский

ppred — частичный предшественник: ppred(0)=none, ppred(n+1)=some n.

LaTeX

$$$$ ppred(0)=\mathrm{none} \quad\text{and}\quad ppred(n+1)=\mathrm{some}\, n. $$$$

Lean4

/-- Partial predecessor operation. Returns `ppred n = some m`
  if `n = m + 1`, otherwise `none`. -/
def ppred : ℕ → Option ℕ
  | 0 => none
  | n + 1 => some n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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