ofNat — Mathlib

English

The nth von Neumann ordinal is defined by the recursive rule: ofNat(0) = ∅ and ofNat(n+1) = insert(ofNat(n), ofNat(n)).

Русский

n-й метод Вон Неймана: ofNat(0) = ∅ и ofNat(n+1) = insert(ofNat(n), ofNat(n)).

LaTeX

$$$$ \text{ofNat} : \mathbb{N} \to \mathrm{PSet}, \quad \text{ofNat}(0) = \emptyset, \text{ofNat}(n+1) = \operatorname{insert}(\operatorname{ofNat}(n), \operatorname{ofNat}(n)). $$$$

Lean4

/-- The n-th von Neumann ordinal -/
def ofNat : ℕ → PSet
  | 0 => ∅
  | n + 1 => insert (ofNat n) (ofNat n)

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