[isabelle] Cardinality in HOL (Was: FuncSet without extensional?)

Hi again,

Am Sonntag, den 19.09.2010, 00:13 +0200 schrieb Joachim Breitner:
> BTW, are there already theories about uncountable sets? I’d need, as a
> lemma, the fact that the M* (the set of finite words) of a uncountably
> infinte set M has the same cardinality.

I discovered that the ZF logic has some good coverage of cardinality,
(including schroeder_bernstein) and the following theorem which seems to
implies the statement above (using K=nat and X(i) the words of length i)

lemma cardinal_UN_le:
     "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |\<Union>i∈K. X(i)| le K"

But looking at the amount of work done to get there, it looks as if it
is too hard to re-do it in HOL. Am I right to assume that there is no
sensible way of using results from ZF in HOL?

Maybe I can try the result above at least for countable infinite M in


Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part

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