Von Neumann ordinals #
This file works towards the development of von Neumann ordinals, i.e. transitive sets, well-ordered
∈. We currently only have an initial development of transitive sets.
Further development can be found on the branch
ZFSet.IsTransitivemeans that every element of a set is a subset.
- Define von Neumann ordinals.
- Define the basic arithmetic operations on ordinals from a purely set-theoretic perspective.
- Prove the equivalences between these definitions and those provided in