Commit 2024-10-22 14:15 b5f6dae5

View on Github →

chore(SetTheory/Ordinal/Arithmetic): WellFounded.rank → IsWellFounded.rank (#16586) We make the WellFounded argument of rank an instance argument. This matches Ordinal.typein.

Estimated changes

Modified Mathlib/Order/Extension/Well.lean

added theorem IsWellFounded.exists_well_order_ge

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem IsWellFounded.rank_eq

added theorem IsWellFounded.rank_lt_of_rel

modified theorem WellFounded.rank_eq

added theorem WellFoundedGT.rank_strictAnti

added theorem WellFoundedLT.rank_strictMono

Modified Mathlib/SetTheory/ZFC/Rank.lean

modified theorem PSet.rank_eq_wfRank

modified theorem ZFSet.rank_eq_wfRank