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 <https://i.imgur.com/hD1QRt2.png> 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 <https://pastebin.com/HKAHJKAn> 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.
