Commit 2024-09-06 08:34 c7cbb887

View on Github →

feat(SetTheory/ZFC): Add PSet.rank and ZFSet.rank (#15977) Add ordinal ranks of PSet and ZFSet.

Estimated changes

added theorem PSet.lt_rank_iff
added theorem PSet.rank_congr
added theorem PSet.rank_empty
added theorem PSet.rank_eq_wfRank
added theorem PSet.rank_insert
added theorem PSet.rank_le_iff
added theorem PSet.rank_lt_of_mem
added theorem PSet.rank_mono
added theorem PSet.rank_pair
added theorem PSet.rank_powerset
added theorem PSet.rank_sUnion_le
added theorem PSet.rank_singleton
added theorem ZFSet.lt_rank_iff
added theorem ZFSet.rank_empty
added theorem ZFSet.rank_eq_wfRank
added theorem ZFSet.rank_insert
added theorem ZFSet.rank_le_iff
added theorem ZFSet.rank_lt_of_mem
added theorem ZFSet.rank_mono
added theorem ZFSet.rank_pair
added theorem ZFSet.rank_powerset
added theorem ZFSet.rank_range
added theorem ZFSet.rank_sUnion_le
added theorem ZFSet.rank_singleton
added theorem ZFSet.rank_union