Jon wrote: >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://www.google.com/url?q=http%3A%2F%2Fus.metamath.org%2Fmpegif%2Fmmtheorems294.html&sa=D&sntz=1&usg=AFQjCNGDJwlgfrBWZedv_GZBSpTwjoNmgg>. 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.
That's great for NN0 ! As for labels, let's see what the other thread gives. I would use itgpow and dvpow. >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 ->" )? It's true that this sounds like a long boring work... unless experienced users know of a faster way?? So yes, it is generally good practice to write theorem in deduction form, if nothing else because it's trivial to get the inference form from it, but harder to go the other way around: you learnt it the hard way! And it's more widely applicable. Even better are closed forms, although it's probably not worth the effort for longer proofs: deduction form is generally enough. I think it's explained in the metamath.pdf book, but here is a summary: If you have a theorem in closed form |- PH -> PS then you get the deduction form |- ( ph -> PH) => |- ( ph -> PS ) by using ~syl, as well as the inference form |- PH => |- PS by using ax-mp. If you have a theorem in deduction form |- ( ph -> PH) => |- ( ph -> PS ) then you get the inference form by using the deduction form above with T. substituted for ph, and use trud (this is why I told you above that the presence of T. as an antecedent and the uses trud in your proof of itgpow shows that parts of the proof are in deduction style). *IF* there are no dv conditions (e.g $d ph x $. if PH contains x) that forbid you from doing so, you can also substitute PH for ph, use id, and recover the closed form. > To anyone, I am a little stuck with this next theorem Please, start a new thread "... (was: Help with beginning to contribute to set.mm)". By the way, the theorem looks false to me: what if C is a non-measurable subset? Or simply RR ? It looks like your B is ( A X. C ). Benoit -- 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/70b2bae4-b1b3-4007-926e-d1a9990b4222%40googlegroups.com.
