Commit 2024-12-15 01:34 7ce82ed5

View on Github →

feat(SetTheory/ZFC/Basic): generalize universes of range (#17016)

Estimated changes

modified theorem ZFSet.mem_range
modified theorem ZFSet.toSet_range
modified theorem ZFSet.rank_range