ofNat — Mathlib

English

The function ofNat enumerates the elements of s in increasing order: ofNat(s)(0)=⊥ and ofNat(s)(n+1)=succ(ofNat(s)(n)).

Русский

Функция ofNat(u) перечисляет элементы s в порядке возрастания: ofNat(s)(0)=⊥, ofNat(s)(n+1)=succ(ofNat(s)(n)).

LaTeX

$$$ofNat(s)(0)=⊥\quad\text{and}\quad ofNat(s)(n+1)=succ(ofNat(s)(n))$$$

Lean4

/-- Returns the `n`-th element of a set, according to the usual ordering of `ℕ`. -/
def ofNat (s : Set ℕ) [DecidablePred (· ∈ s)] [Infinite s] : ℕ → s
  | 0 => ⊥
  | n + 1 => succ (ofNat s n)

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