Commit 2024-10-23 15:46 0ca090b9

View on Github →

feat(SetTheory/Ordinal/Rank): in a well-order, IsWellFounded.rank = Ordinal.typein (#18079)

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Rank.lean

added theorem Acc.mem_range_rank_of_le

added theorem IsWellFounded.mem_range_rank_of_le

added theorem IsWellFounded.rank_eq_typein