Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Members of Natural Leaves

Abstract

Members of Natural Leaves.

Theorem 1.1 (Smaller natural leaves).

Lean statement: D5/S0/History/Spacetime/AllSetNaturalLeafMembers.el_natZ

Proof. Machine-checked in Lean as D5/S0/History/Spacetime/AllSetNaturalLeafMembers.el_natZ (✓ std3). ∎

Source. Repository-derived.

Commentary.

In any universe, the encoding of the finite von Neumann ordinal of a natural number is its natural leaf. Its semantic members are exactly the natural leaves of all strictly smaller natural numbers. The set of members is the range of the natural leaf map on those smaller indices, including the empty range at zero.

References