Re: [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
> 



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