# Re: [isabelle] Can I define direct sum of sets in R^n and R^m

grechukbogdan schrieb:
> Dear Isabelle Users
>
> If A and B are sets, direct sum C of A and B is a set of pairs (a, b) where a \in A and b \in B.
> My first question – is this direct sum defined somewhere in Isabelle?
Yes. It is written "A <*> B". See Product_Type.thy. (Search for "<*>")
> Now, in my case A is a subset of R^n and B is a subset of R^m. In this case, clearly, C is a subset of R^{n+m}.
I'm afraid not the way that these types are defined in HOL. C is only
isomorphic to R^(n+m). You can spell out the type isomorphism explicitly
or define a special product construction on finite Cartesian products.
In either case I leave it to the experts to show you how to do it.
Tobias
> Currently, finite Cartesian product R^n formalized as type real^'n where 'n is some finite type. Now, is it possible to say that C is a subset of real^('n+'m) ? It seems that I can add types (theory Sum_Type), so I would imagine definition of direct sum as a function from (real^'n, real^'m) to real^('n+'m) such that first n coordinates of sum(x, y) coincides with x, and the next m coordinates - with y. Any ideas how to write down such a definition, which theories to look at, or may be suggestions how to formalize this in a different, more convenient way, would be appreciated.
>
> Sincerely,
> Bogdan Grechuk

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