# Re: [isabelle] Sets

• To: Clemens Ballarin <ballarin at in.tum.de>
• Subject: Re: [isabelle] Sets
• From: "Kobayashi, Hidetsune" <hd_coba at yahoo.co.jp>
• Date: Fri, 10 Mar 2006 23:42:44 +0900 (JST)
• Cc: isabelle-users at cl.cam.ac.uk

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