Re: [isabelle] Sets

I really don't see how to form a type that "big enough" to hold this direct product unless it is some specific construction involving 'i and 'a.


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

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