Commit 2024-11-19 22:02 4e69bf9a

feat(SetTheory/ZFC/Ordinal): Initial development of ordinals in ZFSet (#15793) This is ported from the Mathlib 3 branch von_neumann_v2. This is meant as a small, initial PR to iron out any kinks (with the definition, notation, auto-ported lemmas, etc.) before fully developing the file. Of particular note is the quite bare-bones definition of an ordinal. Surprisingly, our weakened transitivity assumption is equivalent to the much stronger claim that ordinals are well-ordered under ∈; see #17001 for a proof.