ofNat — Mathlib

English

ofNat(n) is the PosNum corresponding to n, with ofNat 0 = 1; for n > 0 it matches the natural.

Русский

ofNat(n) — это PosNum, соответствующий n, причём ofNat 0 = 1; для n > 0 он совпадает с натуральным числом.

LaTeX

$$def ofNat (n : ℕ) : PosNum := ofNatSucc (Nat.pred n)$$

Lean4

/-- `ofNat n` is the `PosNum` corresponding to `n`, except for `ofNat 0 = 1`. -/
def ofNat (n : ℕ) : PosNum :=
  ofNatSucc (Nat.pred n)

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