Well, I finally got the Poincaré-Miranda theorem done as I promised a year ago, along with a very restricted version of Brouwer's fixed point theorem. What's left is to show that convex compact sets with nonempty interior are homeomorphic and that those with empty interior are homeomorphic to compact convex sets of lower dimension (allowing for induction from the trivial base case of a point).
On Monday, July 13, 2020 at 8:32:31 PM UTC-4, David A. Wheeler wrote: > > This is my vaguely periodic reminder that I'd love to see more proofs > from the Metamath 100 list. > > Currently there are 74 proofs proven by Metamath from this list of 100 > proofs: > http://us.metamath.org/mm_100.html > > That means there are a few to go; you can see the missing ones here: > http://us.metamath.org/mm_100.html#todo > > These include: > 47. The Central Limit Theorem > 50. The Number of Platonic Solids > 53. π is Transcendental > 59. The Laws of Large Numbers > 62. Fair Games Theorem > 100. Descartes Rule of Signs > > I'd love to see a few more! > It will require only 9 more to tie Isabelle (83). > > --- 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/83aa19aa-b56a-4526-9e0b-5d5422188c12o%40googlegroups.com.
