psub — Mathlib

English

psub(m,n) returns some k if m = n + k, otherwise none.

Русский

psub(m,n) возвращает some k если m = n + k, иначе none.

LaTeX

$$$$ psub(m,n) = \begin{cases} \mathrm{some}\, k, & \text{if } m = n + k \\ \mathrm{none}, & \text{otherwise} \end{cases} $$$$

Lean4

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

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