On Mon, 10 Jun 2019 09:02:00 +0800, Thierry Arnoux <[email protected]> wrote: > Here what could be a "grand plan for the area of the triangle":
Cool! > 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. I'm hoping we can create a proof that ` CC ` can be seen as a specific Euclidean planar geometry so that all our CC-related proofs can be immediately show to apply to any plane & vice versa. I suspect that's a while yet :-). --- David A. Wheeler -- 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/E1haBKq-0007mC-LL%40rmmprod07.runbox.
