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

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