An issue I have is I wonder whether it would also make sense to move my *nc theorems to the main box, since the definition of area implicitly implies on the axiom of countable choice - or not. A complication is that while I'm working on the Poincare-Miranda theorem, I notice that getting it to the Brouwer fixed point theorem would probably most easily entail the theorem that a compact star domain is homeomorphic to the Cartesian product of the extended real line, and the simplest proof of that would probably involve FTC. So now we've got a "100" theorem that (unlike areacirc) doesn't use analysis language, relying on countable choice through analysis theorems.
On Monday, December 16, 2019 at 10:41:23 AM UTC-5, David A. Wheeler wrote: > > As I recently posted, I believe that all "Metamath 100" results (and thus > all they depend on) > should eventually move into the main body. After all, all Metamath 100 > results are > results that at least some others believe are important. I suspect the > folks who already produced metamath 100 results would be the best situated > for proposing where things go. > > So: if you produced a metamath 100 result, but it's currently not in the > main body, I would love to see your proposals to start moving their > dependencies and the result itself into the main body. If there are many > parts, I expect that mini case it would be easier to do it slowly in pieces. > > There is no rush. That said, I think it's important to keep working on > getting more things moved from mathboxes > into the main body. Tools like mmj2 only consider items in the main body > for > many automated steps, and in any case I think it's far more sensible to > readers if major results are properly organized in the main body. > > --- 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/f5545cb7-2169-477e-84ac-e8d1b0aaa18c%40googlegroups.com.
