>> Anyway, I am uncertain about the name »poll«. > > From https://en.wikipedia.org/wiki/Cardinality > > "Two sets A and B have the same cardinality if there exists a bijection from > A to B, that is, a function from A to B that is both injective and > surjective. Such sets are said to be equipotent, equipollent, or > equinumerous. This relationship can also be denoted A ≈ B or A ~ B.”
I see. Using »poll« is a stem, the canonical names would be
less_eq_poll
equiv_poll
greater_eq_poll
(I don't know how useful the strict versions less_poll, greater_poll
would be).
Florian
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
