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



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