Theorem ZFSet.isOrdinal_iff_isTrans

Modification history

2024-12-15 00:44

Mathlib/SetTheory/ZFC/Ordinal.lean

feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals (#17001) …

Modified ZFSet.isOrdinal_iff_isTrans View on Github →

2024-11-19 22:02

Mathlib/SetTheory/ZFC/Ordinal.lean

feat(SetTheory/ZFC/Ordinal): Initial development of ordinals in ZFSet (#15793) …

Added ZFSet.isOrdinal_iff_isTrans View on Github →