*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*: Sat, 09 Apr 2016 20:48:55 +0100*Accept-language*: en-US, en-GB*Acceptlanguage*: en-US, en-GB*In-reply-to*: <5708FEC9.3080907@starkeffect.com>*References*: <5708FEC9.3080907@starkeffect.com>*Thread-index*: AdGSYYsLEZRm1wnNTJSU2UseJiEzrgANsKIQ*Thread-topic*: [isabelle] A question about sets and embeddings in HOL

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:*Dmitriy Traytel

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

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

- Previous by Date: [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: [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