Re: [isabelle] cardinality

Use the search box to find lemmas.

The example you give will be much easier if you express it as

    card{0,1,2::nat} = (3::nat)

You can separately prove

     {(x::nat). x<3} = {0,1,2}

Both require nothing more than auto.

Larry Paulson

On 8 Mar 2006, at 15:09, kuecuek at wrote:

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

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