*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] A question about sets and embeddings in HOL*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Sat, 9 Apr 2016 18:43:49 -0400*Cc*: A.Popescu at mdx.ac.uk*In-reply-to*: <5F22105EAD3CAD4689EC4570AA1802B0BF06E7189F@WGFP-EXMAV1.uni.mdx.ac.uk>*References*: <5708FEC9.3080907@starkeffect.com> <5F22105EAD3CAD4689EC4570AA1802B0BF06E7189F@WGFP-EXMAV1.uni.mdx.ac.uk>*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

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 >

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

**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

- Previous by Date: Re: [isabelle] Display of exceptions in Isabelle/jEdit
- 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