*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Sun, 19 Sep 2010 09:46:35 +0200*In-reply-to*: <1284848024.14778.16.camel@kirk>*References*: <1284833910.14778.10.camel@kirk> <4C951E07.7050702@in.tum.de> <1284848024.14778.16.camel@kirk>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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 HOL. Greetings, Joachim -- 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**

**Follow-Ups**:**Re: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)***From:*Brian Huffman

**References**:**[isabelle] FuncSet without extensional?***From:*Joachim Breitner

**Re: [isabelle] FuncSet without extensional?***From:*Tobias Nipkow

**Re: [isabelle] FuncSet without extensional?***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] FuncSet without extensional?
- Next by Date: Re: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)
- Previous by Thread: Re: [isabelle] FuncSet without extensional?
- Next by Thread: Re: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list