Re: [isabelle] Cardinality for infinite sets
a less involved solution would be to define a cardinality function that
returns an extended natural number (from Extended_Nat in HOL-Library).
definition ecard :: "'a set ⇒ enat" where
"ecard A = (if finite A then card A else ∞)"
Of course, there will be no library of facts for this (yet).
On 2018-03-21 19:19, Diego Marmsoler wrote:
> 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