Theorem ZFSet.IsOrdinal.subset_iff_eq_or_mem

Modification history

2024-12-15 00:44

Mathlib/SetTheory/ZFC/Ordinal.lean

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

Added ZFSet.IsOrdinal.subset_iff_eq_or_mem View on Github →