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

Lawrence Paulson lp15 at cam.ac.uk
Thu Dec 27 13:42:52 CET 2018

> On 27 Dec 2018, at 12:39, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

Thanks for the suggestions.

> The input abbreviation gepoll should be added as well.
> 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.”


More information about the isabelle-dev mailing list