Von Neumann ordinals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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
- 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
A transitive set is one where every element is a subset.