*To*: "stark at cs.stonybrook.edu" <stark at cs.stonybrook.edu>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] A question about sets and embeddings in HOL*From*: Andrei Popescu <a.popescu at mdx.ac.uk>*Date*: Sun, 10 Apr 2016 00:07:31 +0100*Accept-language*: en-US, en-GB*Acceptlanguage*: en-US, en-GB*In-reply-to*: <570985A5.4040105@starkeffect.com>*References*: <5708FEC9.3080907@starkeffect.com> <5F22105EAD3CAD4689EC4570AA1802B0BF06E7189F@WGFP-EXMAV1.uni.mdx.ac.uk> <570985A5.4040105@starkeffect.com>*Thread-index*: AdGSsWnLvKWArUn9Q2C+GjwFNb4XmQAAqLKA*Thread-topic*: [isabelle] A question about sets and embeddings in HOL

Hi Gene, Correct. In my other email I sketch such a (most) economical union, namely, on cardinal representatives. This is useful result in our cardinal library, so I can add it myself. Best, Andrei -----Original Message----- From: Eugene W. Stark [mailto:isabelle-users at starkeffect.com] Sent: 09 April 2016 23:44 To: cl-isabelle-users at lists.cam.ac.uk Cc: Andrei Popescu Subject: Re: [isabelle] A question about sets and embeddings in HOL Andrei, the disjoint union was not what I wanted, because although it does in fact embed all the sets, it separates them and thus produces a set that is not minimal with respect to embeddings. If we make identifications we can get a more economical union. For example if A = {*}, then the disjoint union A+A of A and A is a two-element set, but A itself already embeds A and has only one element, so is itself embedded in A+A. - Gene Stark On 04/09/2016 03:48 PM, Andrei Popescu wrote: > Hi Gene, > > You can use the disjoint union (which is of course not only weakly, but also strongly universal). > Search for the text "Disjoint union of a family of sets" in > https://isabelle.in.tum.de/dist/library/HOL/HOL/Product_Type.html > > All the best, > Andrei > > -----Original Message----- > From: cl-isabelle-users-bounces at lists.cam.ac.uk > [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Eugene > W. Stark > Sent: 09 April 2016 14:08 > To: cl-isabelle-users at lists.cam.ac.uk > Subject: [isabelle] A question about sets and embeddings in HOL > > Is it possible, in HOL, to prove that for any I-indexed collection of sets {F i: i â I} there exists a set S that embeds (via injective maps) all of the sets F i and furthermore is weakly universal for this property, so that if S' is any other set that embeds all the F i then S' embeds S? > In more detail, I am thinking of something like the following: > > definition embeds > where "embeds A B â âf. f â B â A â inj_on f B" > > lemma "âF. âS. (âx. embeds S (F x)) â (âS'. (âx. embeds S' (F x)) â embeds S' S)" > > In ZFC I suppose it would just be possible to take as S the least cardinal greater than the cardinals of all the F i, but I don't have a very clear idea of how/whether something similar could be done in HOL. > > Before I spend a lot of time rummaging through the well ordering stuff in the Isabelle library I thought I would risk asking to see if somebody on this list knows the answer instantly. Thanks for any help you can give. > > - Gene Stark >

**References**:**[isabelle] A question about sets and embeddings in HOL***From:*Eugene W. Stark

**Re: [isabelle] A question about sets and embeddings in HOL***From:*Andrei Popescu

**Re: [isabelle] A question about sets and embeddings in HOL***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] A question about sets and embeddings in HOL
- Next by Date: Re: [isabelle] A question about sets and embeddings in HOL
- Previous by Thread: Re: [isabelle] A question about sets and embeddings in HOL
- Next by Thread: Re: [isabelle] A question about sets and embeddings in HOL
- Cl-isabelle-users April 2016 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