Theorem Acc.mem_range_rank_of_le

Modification history

2024-10-23 15:46

Mathlib/SetTheory/Ordinal/Rank.lean

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

Added Acc.mem_range_rank_of_le View on Github →