Hi Thierry, that grand plan sounds cool. Is what I'm doing helpful towards it? I hope it is something to build on.
Benoit, thanks for your thoughtful response. It sounds like some general result for "associativity of convex combinations" would be pretty useful for proving the equivalence of these two triangle definitions, I'm glad it's something that might be possible. Proving "that area is invariant under displacements (rotations, translations, reflections)" sounds like a very nice program. Looking at areaval <http://us.metamath.org/mpegif/areaval.html> I think maybe translations will be relatively straightforward, as it's just shifting the integral along the x and y directions. However I am not sure how to begin on rotations or (arbitrary) reflections. I am not sure that it will simplify things particularly though. For example " suppose that your triangle has one vertex at (0, 0), one at (a, 0) with a > 0, and the third at (b, c) with c > 0, and then its area is ac/2". The issue here is that computing the area of such a triangle is still non-trivial. It could be done using this triangle splitting method I am working on, however this method can compute the area for any triangle (I think). If you transform a triangle such that one side is vertical then areaquad <http://us.metamath.org/mpegif/areaquad.html>will work however proving that was not easy. So I am not sure, considering the work which is already done, that this method would be easier. Maybe there is some much superior method for computing areas however I am not sure what it is. Thanks :) -- 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/8fe3710d-9734-438e-931f-d3aa2f7f1dd4%40googlegroups.com.
