Jun Xu (Feb 13 2026 at 02:23): Jun Xu (Feb 13 2026 at 02:23):Hey all,
I am wondering if there is a library that implements well-order AND have a function to the effect of
rank :: 'a => 'a set => nat
that extracts the rank of an element inside some well-ordered ambient set?
Balazs Toth (Feb 13 2026 at 10:39):HOL-Library.Inifnite_Set has a implementation of it.
The main function is Infinite_Set.wellorder.enumerate :: 'a set => nat => 'a .
To create a rank function the lemmas Infinite_Set.bij_enumerate,Countable_Set.countableE_infinite, Countable_Set.countable_enum_cases are useful and there is the function Countable_Set.to_nat_on :: 'a set => 'a => nat that could be what you're looking for.
Last updated: Feb 25 2026 at 08:53 UTC