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

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to