# Re: [isabelle] cardinality

On Wednesday 08 March 2006 16:09, kuecuek at rbg.informatik.tu-darmstadt.de 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
done
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 (http://isabelle.in.tum.de/dist/library/HOL/Finite_Set.html).
Note that the cardinality of infinite sets is defined as 0::nat.
Best,
Tjark

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