Re: [isabelle] A question about sets and embeddings in HOL

Hi Gene,

while Andrei is right on the high level, I should point out that your lemma does not hold in HOL as stated.

For instance the type of the existentially quantified "S :: âc set" might simply be not large enough to embed "(F :: âa => âb set) iâ (counterexample: âc = unit, âa = âb = nat, F = %_. UNIV).

Here is a theorem, which I can prove easily using our cardinals library [1]. It fixes âc to be a large enough type to use Sigma as the witness (as Andrei suggested). It also requires the index type âa to be infinite and Sâ to be larger than the index type as well.

theory Scratch

definition embeds
 where "embeds A B â âf. f â B â A â inj_on f B"

lemma embeds_ordLeq: "embeds A B â |B| âo |A|"
  unfolding card_of_ordLeq[symmetric] embeds_def by auto

  fixes F :: "'a â 'b set"
  assumes "infinite (UNIV :: 'a set)"
  shows "âS :: ('a à 'b) set.
    (âx. embeds S (F x)) â
    (âS'. (âx. embeds S' (F x)) â embeds S' (UNIV :: 'a set) â embeds S' S)"
  unfolding embeds_ordLeq using assms
  by (auto simp: image_iff card_of_ordLeq_finite
   intro!: exI[of _ "Sigma UNIV F"] surj_imp_ordLeq[of _ snd] card_of_Sigma_ordLeq_infinite)


I did not think thoroughly if all my modifications are necessary. I.e., what happens if the index type âa is finite?

Best wishes,

[1] Cardinals in Isabelle/HOL
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
ITP 2014,

> On 09 Apr 2016, at 21:48, Andrei Popescu <a.popescu at> 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
> All the best, 
>  Andrei 
> -----Original Message-----
> From: cl-isabelle-users-bounces at [mailto:cl-isabelle-users-bounces at] On Behalf Of Eugene W. Stark
> Sent: 09 April 2016 14:08
> To: cl-isabelle-users at
> 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.