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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.