On Tuesday, June 4, 2019 at 11:15:03 AM UTC+2, Jon P wrote:
>
> Benoit I like your way of using barycentric coordinates to express the
> interior of the triangle, that is quite elegant. I am not sure how to fit
> it into this scheme though,
>
The points "inside" the triangle with vertices A, B, C are also
characterized as follows: the points A, B define a line, and I want the
point X to be in the half-plane with boundary the line (AB) and containing
C (this is easily expressed algebraically, see below); similarly for the
other two half-planes. This characterization is likely easier to compute
areas. Therefore, as a first step, and before computing areas, I would
formalize this equivalence of the two characterizations in metamath, using
the representation of the plane as the set of complex numbers.
For instance, in "pseudo-metamath":
df-triangle $a |- triangle = ( <. x, y, z >. e. ( C. X. C. X. C. ) |-> { u
e. C. | E. a e. R. E. b e. R. E. c e. R. ( 0 =< a /\ 0 =< b /\ 0 =< c /\ a
+ b + c = 1 /\ u = a x + b y + c z } )
Then I would prove the permutation formulas (easy):
A, B, C e. C => triangle (A, B, C) = triangle (B, C, A) = triangle (C, A ,
B) = triangle (A, C, B) =...
Finally, I would prove the above equivalence. First, define the vector
product vec : C. X. C. --> R. Then, prove:
triangle-charac $p |- ( X e. triangle (A, B, C) <->
( 0 <= ( ((B-A) vec (C-A)) x. ((B-A) vec (X-A)) ) /\
0 <= ( ((C-B) vec (A-B)) x. ((C-B) vec (X-B)) ) /\
0 <= ( ((A-C) vec (B-C)) x. ((A-C) vec (X-C)) ) ) $= ? $.
Of course, this necessitates several lemmas and will be long. You first
prove the implication to the right by proving
trianglelem $p |- ( X e. triangle (A, B, C) -> 0 <= ( ((B-A) vec (C-A)) x.
((B-A) vec (X-A)) ) ) $= ? $.
which should be long but straightforward algebraic manipulation. The ohter
two are then obtained thanks to triangle(A, B, C) = triangle (C, A, B) etc.
The converse implication might be harder: every point in the plane can be
written using barycentric coordinates summing up to 1; then the three
half-plane conditions will impose that the coefficients are nonnegative.
Note: informally, the implication to the right is easy: changing notation,
let a x + b y + c = 0 be the equation of the line (AB). If you plug in for
(x, y) the coordinates of a point expressed as a barycentric mean of A, B,
C (say, with coefficients s, t, u >= 0), then, using the fact that A and B
are indeed on the line (AB) so satisfy the equation, one has:
a (s xA + t xB + u xC) + b (s yA + t yB + u yC) + c (s + t + u) = a u xC +
b u yC + c u = u (a xC + b yC + c) has the same sign as a xC + b yC + c.
Benoit
--
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/5ae10767-1aef-42ba-a089-6f9b87a268ad%40googlegroups.com.
