Commit 2025-05-08 17:56 4dce23bc
View on Github →feat (Order/WellFoundedSet): Preimage of a partially well-ordered subset along a decreasing sequence is bounded above. (#24307) Given a partially well-ordered subset and an infinite decreasing sequence, the sequence eventually leaves the subset forever.