Commit 2024-12-15 00:03 ecf9698f

View on Github →

chore(SetTheory/ZFC/Rank): clean up file (#18239) This PR does the following:

  • Make various theorems take explicit arguments (as it's a bit painful to invoke them otherwise)
  • Replace lsub f by ⨆ i, succ (f i), in anticipation for the former being deprecated.

Estimated changes

modified theorem PSet.le_succ_rank_sUnion
modified theorem PSet.rank_insert
modified theorem PSet.rank_pair
modified theorem PSet.rank_powerset
modified theorem PSet.rank_sUnion_le
modified theorem PSet.rank_singleton
modified theorem ZFSet.le_succ_rank_sUnion
modified theorem ZFSet.rank_insert
modified theorem ZFSet.rank_pair
modified theorem ZFSet.rank_powerset
modified theorem ZFSet.rank_range
modified theorem ZFSet.rank_sUnion_le
modified theorem ZFSet.rank_singleton
modified theorem ZFSet.rank_union