*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Can I define direct sum of sets in R^n and R^m*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 29 Jun 2010 12:55:15 +0200*Cc*: isabelle-users at cl.cam.ac.uk, grechukbogdan <grechukbogdan at yandex.ru>*In-reply-to*: <F5F24271-F65B-405E-AFDE-F3A0D4694138@cam.ac.uk>*References*: <581661277744215@web145.yandex.ru> <F5F24271-F65B-405E-AFDE-F3A0D4694138@cam.ac.uk>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

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

**References**:**[isabelle] Can I define direct sum of sets in R^n and R^m***From:*grechukbogdan

**Re: [isabelle] Can I define direct sum of sets in R^n and R^m***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- Next by Date: Re: [isabelle] Type class instantiation without using Isar syntax
- Previous by Thread: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- Next by Thread: Re: [isabelle] Can I define direct sum of sets in R^n and R^m
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list