Commit 2024-09-12 06:16 381b26ac
View on Github →feat(Order/SuccPred/Limit): IsSuccLimit
(#16499)
The matter of whether 0
is or not a limit element (of the ordinals/cardinals) is a highly contentious one. To bridge this gap, we redefine IsSuccLimit
so as to explicitly exclude minimal elements. A previous PR had already renamed the weaker notion to IsSuccPrelimit
.
Future PRs will introduce the usual limit induction principles, and deprecate Cardinal.IsLimit
and Ordinal.IsLimit
.