Re: [isabelle] cardinality

On Wednesday 08 March 2006 16:09, kuecuek at wrote:
> for example if i try to prove this with card  :
> there are 3 natural numbers smaller than 3
> card {(x::nat). x<3} = (3::nat)
> is this right or how should i construct this lemma?

The lemma looks good to me, and once you've established that {(x::nat). x<3} is
equal to {0, 1, 2}, it can be proven automatically:

lemma "card {(x::nat). x<3} = 3"
  apply (subgoal_tac "{(x::nat). x<3} = {0, 1, 2}")
  apply auto

It is of course just an instance of a more general lemma, which you could prove
using induction:

lemma "card {x. x<n} = n"

> another question is where can i find useful lemmas about card? (in set?)

Rather in Finite_Set (
Note that the cardinality of infinite sets is defined as 0::nat.


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