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

Am Montag, den 28.06.2010, 20:56 +0400 schrieb grechukbogdan:
> 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?

This is defined in Isabelle/HOL as "A \<times> B" or "A <*>B" (in
ASCII).

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

In the current _development_ version of Isabelle (unfortunately not in
Isabelle2009-2) real^'n is a euclidean space. When we add the type class
instantiation for products of euclidean spaces:

instantiation * :: (real_basis, real_basis) real_basis
...

instantiation * :: (euclidean_space, euclidean_space) euclidean_space
...

instantiation * :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
...

(with the appropriate definition for basis etc)

This should be a very convenient way as no isomorphisms need to be
specified to transfer between real^'n * real^'m and real^('n + 'm).
Everything including integration was updated to operate on euclidean
spaces.

This is already proved in Isabelle, I will push it tomorrow.

Greetings,
Johannes

> Sincerely,
> Bogdan Grechuk



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