Commit 2026-09-11 10:13 3212d40d

View on Github →

refactor: replace IsWellFounded with WellFounded (#42351) This PR is an attempt to deprecate IsWellFounded. The reason it that it is entirely equivalent to WellFounded, with the only difference being that IsWellFounded is a class. This PR instead marks WellFounded as a class. This PR has been re-opened from #35602, with permission.

Estimated changes

modified theorem DFinsupp.Lex.acc
modified theorem DFinsupp.Lex.acc_single
modified theorem DFinsupp.Lex.wellFounded'
modified theorem DFinsupp.Lex.wellFounded
modified theorem Pi.Lex.wellFounded
deleted theorem WellFounded.list_chain'
deleted theorem WellFounded.cutExpand
modified theorem isCofinal_setOfPred_imp_lt
modified theorem Pi.trichotomous_lex
deleted theorem IsWellFounded.apply
deleted def IsWellFounded.fix
deleted theorem IsWellFounded.fix_eq
deleted theorem IsWellFounded.induction
modified theorem Subrelation.isWellFounded
added theorem WellFounded.apply'
modified theorem WellFounded.asymmetric
modified theorem WellFounded.asymmetric₃
added def WellFounded.fix'
added theorem WellFounded.fix'_eq
added theorem WellFounded.induction'
modified theorem wellFounded_lt
modified theorem isArtinian_of_surjective
deleted theorem isNoetherian_iff'
modified theorem isNoetherian_iff
deleted theorem Ordinal.lt_wf
deleted theorem NONote.lt_wf
deleted theorem IsWellFounded.rank_eq
added theorem WellFounded.rank_eq
deleted theorem ZFSet.mem_wf
deleted theorem Class.mem_wf
deleted theorem PSet.mem_wf
modified theorem PSet.rank_eq_wfRank
modified theorem ZFSet.rank_eq_wfRank