Hi Benoit. I made some changes to itexp as you suggested, I changed the conditions so it works with NN0 and I changed the name to itgexp as "itg" seems to be the common abbreviation for integral. I am very happy to change to either itgmon or itgpow, it's fine with me, however I think that it should definitely match dvexp <http://us.metamath.org/mpegif/dvexp.html>and maybe also the exp theorems in Glauco's Mathbox <http://us.metamath.org/mpegif/mmtheorems294.html>. So I think I am very happy to change and I think someone with more authority than me would need to make the change global and do I find replace in all theorems that rely on dvexp etc if this change is to happen.
I'm afraid at the moment I don't want to start on replacing everything with (ph ->, that sounds like quite a lot of tricky work, I might get to it in the future though. I can see that a lot of thought has gone into deduction vs inference etc. Is it good practice in general to write everything in deduction form ( I mean starting with "( ph ->" )? To anyone, I am a little stuck with this next theorem, I have DJVars again at line 74 and I am not sure I am taking the right approach. I am happy to keep working away on it however it would be helpful if anyone was willing to advise whether I am taking the right approach or not, do I have the right sort of notation? Some theorems seem not to accept <. x , y >. in the place of an &S1 which means it is a bit challenging, but probably still doable. Here <https://pastebin.com/AEMbVULE>is the text, this is the theorem: h1::subarea.1 |- A e. dom area h2::subarea.2 |- C C_ RR h3::subarea.3 |- B = { <. x , y >. | ( <. x , y >. e. A /\ x e. C ) } !qed:: |- B e. dom area -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/66f369ee-dba2-45b0-ab3c-d0721c6d3106%40googlegroups.com.
