ofNat — Mathlib

English

There is a canonical embedding of natural numbers into ONote given by ofNat: 0 maps to 0 and n+1 maps to oadd 0 n.succPNat 0.

Русский

Существует каноническое вложение натуральных чисел в ONote через ofNat: 0 ↦ 0, n+1 ↦ oadd 0 n.succPNat 0.

LaTeX

$$@[coe] \text{ofNat}: \mathbb{N} \to ONote,\; 0 \mapsto 0,\; (n+1) \mapsto oadd 0 n^{succPNat} 0$$

Lean4

/-- Convert a `Nat` into an ordinal -/
@[coe]
def ofNat : ℕ → ONote
  | 0 => 0
  | Nat.succ n => oadd 0 n.succPNat 0

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