Theorem ZFSet.empty_isTransitive

Modification history

2024-11-19 22:02

Mathlib/SetTheory/ZFC/Ordinal.lean

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

Deleted ZFSet.empty_isTransitive View on Github →

2023-04-10 15:18

Mathlib/SetTheory/ZFC/Ordinal.lean

feat: port SetTheory.ZFC.Ordinal (#3334) …

Added ZFSet.empty_isTransitive View on Github →