Commit 2024-10-22 17:17 877aae73

View on Github →

chore(SetTheory/Ordinal/Rank): move IsWellFounded.rank to its own file (#18078)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Extension/Well.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Acc.rank_eq

deleted theorem Acc.rank_lt_of_rel

deleted theorem IsWellFounded.rank_eq

deleted theorem IsWellFounded.rank_lt_of_rel

deleted theorem WellFounded.rank_eq

deleted theorem WellFounded.rank_lt_of_rel

deleted theorem WellFounded.rank_strictAnti

deleted theorem WellFounded.rank_strictMono

deleted theorem WellFoundedGT.rank_strictAnti

deleted theorem WellFoundedLT.rank_strictMono

Created Mathlib/SetTheory/Ordinal/Rank.lean

added theorem Acc.rank_eq

added theorem Acc.rank_lt_of_rel

added theorem IsWellFounded.rank_eq

added theorem IsWellFounded.rank_lt_of_rel

added theorem WellFounded.rank_eq

added theorem WellFounded.rank_lt_of_rel

added theorem WellFounded.rank_strictAnti

added theorem WellFounded.rank_strictMono

added theorem WellFoundedGT.rank_strictAnti

added theorem WellFoundedLT.rank_strictMono

Modified Mathlib/SetTheory/ZFC/Rank.lean