[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.