Re: [isabelle] Sets



 Hi! Thaks for the answers.

  Let me explain the problem again.
  
  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)? 
          
> >   Let A be a set (A :: 'a set), then is there a 
> > set (B :: 'b set) which is isomorphic to A?
> 
> Not in general.  The type 'b might be too small to
> accommodate all the
> elements of A.  This doesn't hold because type
> variables are implicitly
> universally quantified at the very beginning of a
> formula.
> 


--------------------------------------
TSUKAME EIKOU! KAGAYAKE EGAO!
Yahoo! JAPAN JPC OFFICIAL PARTNER INTERNET PORTAL SITE
http://pr.mail.yahoo.co.jp/wintergames/





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