Theorem PSet.le_succ_rank_sUnion

Modification history

2024-12-15 00:03

Mathlib/SetTheory/ZFC/Rank.lean

chore(SetTheory/ZFC/Rank): clean up file (#18239) …

Modified PSet.le_succ_rank_sUnion View on Github →

2024-09-06 08:34

Mathlib/SetTheory/ZFC/Rank.lean

feat(SetTheory/ZFC): Add `PSet.rank` and `ZFSet.rank` (#15977) …

Added PSet.le_succ_rank_sUnion View on Github →