[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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and