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 cl.cam.ac.uk
Subject: Re: Cardinality for infinite sets
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 lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Diego Marmsoler <diego.marmsoler at tum.de>
Sent: 21 March 2018 18:19:24
To: isabelle-users at cl.cam.ac.uk
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and