[isabelle] Extended real line and epigraph



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

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,
Bogdan Grechuk.





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