*To*: "Kobayashi, Hidetsune" <hd_coba at yahoo.co.jp>*Subject*: Re: [isabelle] Sets*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 14 Mar 2006 14:51:16 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20060312024336.79696.qmail@web2811.mail.bbt.yahoo.co.jp>*References*: <20060312024336.79696.qmail@web2811.mail.bbt.yahoo.co.jp>

Larry

Given (I :: 'i set), (A i :: 'a set) . The direct product of the family {A i} is ('i => 'a) set. My question is: is it possible to find some set B isomorphic to the direct product and B having some 'a123 type (the only condition for the type of B is that the type is expressed in one string, say as a123, not as 'i => 'a)?

On 12 Mar 2006, at 02:43, Kobayashi, Hidetsune wrote:

Elsa L Gunter's answer means: "if we take I = B and A i = {0,1} then the direct product has the cardinality strictly larger than that of B and we have contradiction."

**References**:**[isabelle] Sets***From:*Kobayashi, Hidetsune

- Previous by Date: [isabelle] Three Research Positions - Foundations of Distributed Computation
- Next by Date: [isabelle] cardinality
- Previous by Thread: [isabelle] Sets
- Next by Thread: [isabelle] mutual recdefs
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list