ofNat — Mathlib

English

There is a conversion from natural numbers to NONote

Русский

Существует отображение натуральных чисел в NONote

LaTeX

$$$$ \operatorname{ofNat}_{\text{NONote}}(n) = \langle \operatorname{ONote.ofNat}(n), \langle \langle _, \operatorname{nfBelow\_ofNat}(n) \rangle \rangle \rangle. $$$$

Lean4

/-- Convert a natural number to an ordinal notation -/
def ofNat (n : ℕ) : NONote :=
  ⟨ONote.ofNat n, ⟨⟨_, nfBelow_ofNat _⟩⟩⟩

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