toPNat' — Mathlib

English

ToPNat' maps a natural number to a positive natural by succPNat(pred n).

Русский

ToPNat' отображает натуральное число в положительное натуральное число как succPNat(pred n).

LaTeX

$$$ \\operatorname{toPNat'}(n) = \\operatorname{succPNat}(\\operatorname{pred}(n)).$$$

Lean4

/-- Convert a natural number to a `PNat`. `n+1` is mapped to itself,
  and `0` becomes `1`. -/
def toPNat' (n : ℕ) : ℕ+ :=
  succPNat (pred n)

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