Re: [isabelle] Cardinality for infinite sets

... though this may be too heavy for your intended application, e.g., if you don't care about distinguishing between different infinite cardinalities. The heaviness comes from having to use ordinal embedding (denoted <o and <=o) and isomorphism (denoted =o) instead of (in)equality of natural numbers.



From: Andrei Popescu
Sent: 21 March 2018 19:19:28
To: Diego Marmsoler; isabelle-users at
Subject: Re: Cardinality for infinite sets

Hi Diego,

Please see

and, for a more complete set of results,

These are all documented in the ITP 2014 paper

Let me know should you have any problems using these.



From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Diego Marmsoler <diego.marmsoler at>
Sent: 21 March 2018 18:19:24
To: isabelle-users at
Subject: [isabelle] Cardinality for infinite sets

Dear Isabelle experts,

while playing around with "card" from theory Finite_Set, i recognized that it returns 0 for infinite sets.
Now i was wondering whether someone knows about a similar construct which, for this case, returns infinity from the extended natural numbers.

Many thanks in advance!

Best regards,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.