[isabelle-dev] cardinality primitives in Isabelle/HOL?

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Dec 27 13:45:36 CET 2018

>> 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


(I don't know how useful the strict versions less_poll, greater_poll
would be).


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20181227/cb87e514/attachment.sig>

More information about the isabelle-dev mailing list