Hi Jon, Yes, I think that’s the right approach. I believe once you have the full statement, you start from your triangle, rewrite it as a union, and then apply “itgsplit”.
In order to handle the “without loss of generality” (like in “without loss of generality, we can assume that the abscisses are in ascending order”), in set.mm, one could first prove the specific theorem in the case X <_ Y <_ Z, as a lemma, and then in the main proof, use mpjaodan type of theorem to produce the 6 different cases, whereas each case can be proved with the lemma. BR, _ Thierry > Le 5 juin 2019 à 16:30, Jon P <[email protected]> a écrit : > > > 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 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. -- 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/BD6291BA-C41C-4DCF-8DDC-61F6EEAF3D84%40gmx.net.
