Hey I think I made some progress on linking Benoit's definition of a triangle with the "vertical slices" one which I posted on Jun 5. Here is a diagram of a point in a triangle. Assume A,B,C are vectors in RR^2 or in CC, I think it works the same. This is the case where the right side of the triangle is vertical, the case where the left side is vertical is basically the same, any triangle is the union of two triangles, one which a straight right side and another with a straight left side.
If we start with the vertical slices approach we know that P = (xA + yC) + zy (B - C) where x + y = 1 and z <_ 1. That is you start at the point xA + yC and go up some amount vertically, which is (B-C), but sufficiently little that you don't leave the top of the triangle. We can rearrange this to P = xA + zy B + ( y - zy) C and this satisfies Benoit's defintion, that a point is in the triangle if P = alpha A + beta B + gamma C and alpha + beta + gamma <_ 1 because x + zy + y -zy = x + y = 1. We know x >_ 0 and y >_ 0 by definition and with z <_ 1 we know y - zy >_ 0 so alpha, beta, gamma >_0. Likewise given a point P = alpha X + beta y + gamma Z where alpha + beta + gamma <_ 1 we can rewrite this as P = xA + zy B + (y - zy) C, where x = alpha, zy = beta and y - zy = gamma. Then rearrange so that P = xA + yC + zy (B - C). We know that x + y = alpha + beta + gamma <_ 1 and we know that zy = beta <_1 so this point is in the triangle by the vertical slices definition. How do we know z,y > 0? We are just solving zy = beta simultaneously with y - zy = gamma. If you sum these you get y = beta + gamma > 0 and then z = beta / y > 0. Apologies this is all quite loose and wordy as usual, I'd appreciate any feedback from anyone who is interested, do you agree this could be formalised to show the equivalence of the two definitions? I haven't thought about your definition Thierry and I think a similar proof would be possible. -- 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/d27bf636-bfca-4bf4-bb6d-f41e5f97d746%40googlegroups.com.
