[isabelle] cardinality


i have a problem with cardinality.

i don't understand how i have to use card in isabelle.

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?

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


best regards

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