Pretty happy to see Brouwer's famous theorem even if its scope has beeen restricted to the unit cube.
-- FL Le vendredi 21 août 2020 à 09:31:49 UTC+2, [email protected] a écrit : > 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/7a554f3e-038f-4118-8047-1e4c9198ae77n%40googlegroups.com.
