Here what could be a "grand plan for the area of the triangle":
* progress in the "Geometry" part of set.mm until triangles are defined. There is already a definition of congruence for triangles ( ~ trgcgr <http://us2.metamath.org:88/mpeuni/trgcgr.html>) * progress in the "Geometry" part of set.mm until a distance/metric is defined, for segment lengths. This is further away, down the path. * define a function for rectangles, to be the product (in RR) of their length and width. * construct an outer measure based on that function (Method I, Monroe), and derive a measure: that's the generic ` area ` measure of surfaces! * prove that triangles are area-measurable (e.g. first prove that half-planes are measurable, then any intersections of them) * prove the formula for the area of a rectangle triangle, then of any triangle (as half of base times height) Anything less generic than this is too specific! ;-) Once we have proven that ` CC ` can be seen as a specific Euclidean planar geometry, we can prove that the current definition of ` area ` and the very general one match on their common domain of definition. But of course all of this is quite far away. In the mean time, it's pretty fine to work with coordinates! -- 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/720f8ab8-8cee-be47-681a-04f4e8279730%40gmx.net.
