[isabelle] Left and right limits

Dear Isabelle Users

Is there a notion of left and right limits defined in Isabelle?

For example, is there a notation to formulate a lemma that function f(x)=x/|x| at 0 has limit -1 if x tend to 0 from the left and +1, if x tend to 0 from the right? 

If not, I need to define this for my formalization. Clearly, such limits are important far more than in convex analysis, in particular they are needed to introduce left and right derivatives, etc. Do you have any suggestions how to define this properly and which notation is better to use (maybe, consistent with some other formalizations, etc) ?


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