Theorem ZFSet.rank_range

Modification history

2024-12-15 01:34
Mathlib/SetTheory/ZFC/Rank.lean
feat(SetTheory/ZFC/Basic): generalize universes of `range` (#17016)
Modified ZFSet.rank_rangeView on Github →
2024-12-15 00:03
Mathlib/SetTheory/ZFC/Rank.lean
chore(SetTheory/ZFC/Rank): clean up file (#18239) …
Modified ZFSet.rank_rangeView on Github →
2024-09-06 08:34
Mathlib/SetTheory/ZFC/Rank.lean
feat(SetTheory/ZFC): Add `PSet.rank` and `ZFSet.rank` (#15977) …
Added ZFSet.rank_rangeView on Github →