Convex polytopes in Metamath?

Higher-dimensional geometry (previously "Polyshapes").

Convex polytopes in Metamath?

Postby Keiji » Fri Mar 05, 2010 8:10 pm

I've been looking for a way to represent convex polytopes in terms of ZFC, so it can be put in Metamath ( http://us2.metamath.org:88/mpeuni/mmset.html ). So far, I've come up with these, perhaps naive, definitions, but I haven't been able to use them to prove anything yet (there's one unproved "theorem" at the end, which I was trying to prove but Metamath proofs are rather unintuitive).

Well, nearly half of that file involves defining tuples (ordered collections). The existing ordered pair definition could probably be used instead but I wanted to define tuples separately (though I've forgotten exactly why now). I've also defined symmetry groups as functions mapping a point onto a set of points, as I couldn't find any definition of symmetry groups in the Metamath database, and once again there is probably a much better, less naive, more canonical way to do this.

Am I going about this the wrong way? I ultimately want to be able to use Metamath to get some nice results about convex polytopes, but if I can't even prove that a point is one of them then I'm certainly not going to be able to get anything useful. If there are any experienced Metamath users around here, or anyone with some more inspirational ideas of how to do this please lend a hand.
User avatar
Keiji
Administrator
 
Posts: 1984
Joined: Mon Nov 10, 2003 6:33 pm
Location: Torquay, England

Re: Convex polytopes in Metamath?

Postby PWrong » Fri Apr 02, 2010 8:03 am

Sorry, I've never understood how Metamath works.
User avatar
PWrong
Pentonian
 
Posts: 1599
Joined: Fri Jan 30, 2004 8:21 am
Location: Perth, Australia


Return to Other Geometry

Who is online

Users browsing this forum: No registered users and 11 guests

cron