Hi Jon, One thought which may help you:
I would start from the end, resolving your last statement using a ‘mpjaodan’, ‘pm2.61dane’, or, if you use induction, ‘pm2.61i’. This will create new sub goals for your different cases, which you can then proceed to prove. BR, _ Thierry > Le 2 juin 2019 à 16:46, Jon P <[email protected]> a écrit : > > Thanks for all help, area quad is now included in set.mm so that is pretty > nice :) > > If I have a chance I am thinking of these as next steps, if anyone is > interested and has thoughts that would be appreciated. > > First take any 3 points in R^2 and make a triangle. I think if you order the > points by x coord there are 5 cases (as RR is well ordered). Here is an image > of them. Computing the area of Case 1 (all x coords the same) is trivial > (though needs to be covered), cases 2 and 3 (two x coords the same) are > covered by area quad directly, which is nice. Cases 4 and 5 are a bit > trickier. > > The approach I am thinking of is to split the domain at the point Q e. RR. > This will make the triangle in to two triangles which are case 2 and 3 so are > computable. > > I started down this road but I am not sure about the direction, this general > result is what I was thinking of trying to prove first. > > *hypothesis > 54:: |- A e. dom area > 55:: |- Q e. RR > 56:: |- B = { <. x , y >. | ( <. x , y >. e. A /\ x <_ Q ) } > 57:: |- C = { <. x , y >. | ( <. x , y >. e. A /\ Q <_ x ) } > *resutls > 600:: |- B e. dom area > 601:: |- C e. dom area > qed:: ( area ` A ) = ( area ` B ) + ( area ` C ) > > Here is how far I have got, it is not so easy. I was then going to try to > write an "area of a triangle" theorem which covers all cases. I do not have > so much energy to work on it but hopefully I can do something :) > -- > 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/18bcf7ed-95fe-48a0-a280-e243485656a1%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/629B8839-5C04-451C-9ECE-79177FAAC094%40gmx.net.
