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

Lawrence Paulson schrieb:
> Once again, this formalisation of finite Cartesian products is showing itself to be unsuitable for abstract mathematics.

I'm interested: how do you model the problem in any formalism such that
A^m * B^n = A^(m+n) without resorting to an explicit isomorphism along
the way? Unless I am mistaken, the datatypes you provide in your
formalization of ZF do not do the job either.

> It is only useful if you intend to work in one fixed dimension. I hope it isn't used extensively.

It is. Luckily it works quite well for concrete mathematics.

Tobias

> Larry
>
> On 28 Jun 2010, at 17:56, grechukbogdan wrote:
>
>> 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?
>>
>> 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.
>



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