*To*: grechukbogdan <grechukbogdan at yandex.ru>*Subject*: Re: [isabelle] Extended real line and epigraph*From*: Robert Himmelmann <himmelma at in.tum.de>*Date*: Tue, 20 Jul 2010 09:58:18 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <590261279384225@web120.yandex.ru>*References*: <590261279384225@web120.yandex.ru>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; de; rv:1.9.2.4) Gecko/20100608 SUSE/3.1.0 Thunderbird/3.1

Am 17.07.2010 18:30, schrieb grechukbogdan:

Dear Isabelle Users In context of my convex analysis formalization I need to work with function from Euclidean Space to extended real line - namely Real together with TWO points -\infty and +\infty. 1) Is such extended real line defined in Isabelle? I will need basic operations like a * +\infty = +\infty for a>0, etc. I am not sure how to say that +\infty - (+\infty) is undefined...

http://isabelle.in.tum.de/~himmelma/cgi-bin/repos.cgi/mnt/tmp/himmelma/repos/isabelle/file/5efa68013118/src/HOL/Probability/Positive_Infinite_Real.thy

2) If so, are such functions from Euclidean Space to extended real line defined in Isabelle? What about convexity definition? I just do not want to define the same again.

3) I will need a fact that epigraph of such a function is also a set in an Euclidean Space. Actually, epigaph is defined in Convex_Euclidean_Space.thy as a pair (x,y), or, in other words, subset of direct sum of Euclidean Space and Real. This is connected with my previous question about direct sum of sets in R^n and R^m. I was told that there exists an instantiation instantiation * :: (euclidean_space, euclidean_space) euclidean_space which would be very useful. I have istalled latest repository version, but I do not see something like this. Is this instantiation already done in repository version? If so, in which theory I can look at it, and can I use this for the purposes described above?

Sincerely, Robert

**References**:**[isabelle] Extended real line and epigraph***From:*grechukbogdan

- Previous by Date: Re: [isabelle] Code generation with invariants and new data types
- Next by Date: [isabelle] Questions about speed and CPU usage
- Previous by Thread: [isabelle] Extended real line and epigraph
- Next by Thread: Re: [isabelle] Update on I3P
- Cl-isabelle-users July 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