Looks like some nice ideas here. Thierry I will try to write out what I had thought in full, some detail may be missing I think.
Take 3 points in CC (though RR^2 could work too), say A, B, C. I was thinking the first step is to relabel them X,Y,Z such that Re(X) <_ Re(Y) <_ Re(Z), I am not sure if this is possible in metamath, so yes getting the abscisses in ascending order. This diagram <https://imgur.com/CvuWUQl> on the right might help. I Then when they are in ascending order define three interpolation functions as before I(x) = ( x - Re(Z) ) / ( Re(Z) - Re(X) ) [whole interval] J(x) = ( x - Re(Y) ) / ( Re(Y) - Re(X) ) [left section] K(x) = ( x - Re(Z) ) / ( Re(Z) - Re(Y) ) [right section] Lets assume that Y is below the line X -> Z. Define the midpoint on the longer side W = X + ( I(Re(Y)) x. Z ) Define the 4 bounding lines: U1 = X + J(x) x. ( W - X ) V1 = X + J(x) x. ( Y - X ) U2 = W + K(x) x. ( Z - W ) V2 = Y + K(x) x. ( Z - Y ) Then define the interior of the triangle as triangle(X,Y,Z) = { t e. CC | ( Re(X) <_Re(t) <_ Re(Y) /\ t e. ( V1 [,] U1) ) \/ ( Re(Y) <_Re(t) <_ Re(Z) /\ t e. ( V2 [,] U2) ) } so basically you define the interior piecewise in the same way as area quad, just setting the left section and right section separately. This would mean it would be not so hard to then use area quad on both pieces to get the area of the triangle. However I think there may be some problems with defining each of the 5 cases. I think it might be possible to prove the equivalence of this definition with Benoit's or yours (they are the same set), and then we could use both, this one for ease of proving the area and a nice one for more public consumption. I am very happy to change direction if there is a better one, I know this is a bit scrappy, I hope it is helpful. -- 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/026a3372-99f9-4a8b-960f-1cb9d67e5adb%40googlegroups.com.
