*To*: Andrei Popescu <uuomul at yahoo.com>*Subject*: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Mon, 20 Sep 2010 10:41:30 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <633215.28848.qm@web56107.mail.re3.yahoo.com>*References*: <mailman.5.1284865202.21615.cl-isabelle-users@lists.cam.ac.uk> <633215.28848.qm@web56107.mail.re3.yahoo.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Andrei, Am Sonntag, den 19.09.2010, 20:20 -0700 schrieb Andrei Popescu: > >> 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. > > Actually, quite a bit of the ZF theory of cardinals can be done in HOL. > I have already set the basis of such a theory: it is in the Isabelle AFP, and is > > fairly well documented. > > http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml > > Your lemma is stated there in the theory Cardinal_order_relation, in subsection > "Cardinals versus lists", as > > > List_infinite_bij_betw > > (NB: it holds for any infinite set, including the countably infinite ones.) Thanks for the pointer. This is what I need... I need to get better at finding existing theories :-) You define definition List :: "'a set => 'a list set" where "List A ≡ {l. set l ≤ A}" This is a definition that I could use in the development of Free Groups. Assuming I would not need the cardinality lemmas, what is the best practice: Importing your theory nevertheless, copying the definition or pushing to add this definition in a more standard, common place, i.e. HOL or HOL/Library? 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] FuncSet without extensional? (Joachim Breitner)***From:*Andrei Popescu

**References**:**Re: [isabelle] FuncSet without extensional? (Joachim Breitner)***From:*Andrei Popescu

- Previous by Date: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- Next by Date: Re: [isabelle] Unicode (Was: Update on I3P)
- Previous by Thread: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- Next by Thread: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- 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