Re: [isabelle] Cardinality for infinite sets



Hallo,

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

Manuel


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




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