On 9/22/23 17:00, [email protected] wrote:
I'm extremely hesitant to suggest changes to the main database, having flunked out of school now twice, but working on what I call "cmpcvxhmph" and "cmpcvxhmph0" (i.e., that any complex convex shape is homeomorphic to the unit ball), I'm finding myself very often relying on the property expressed in fnconstg, and I'm wondering whether it might be better expressed as an fnconst, or even fnconstd, as since I've started on this project ovexd, fvexd, and fzfid have been introduced. --
There's always a push and pull about how many convenience theorems are too many (especially if they just replace two steps). One thing which may give at least some idea of the tradeoff is "Usually we will also automatically accept a _new_ theorem that is used to shorten multiple proofs, if the total size of set.mm (including the comment of the new theorem, not including the acknowledgment) decreases as a result." (from https://us.metamath.org/mpeuni/conventions.html ). Personally, I mostly just work with whatever theorems are there and don't get worried about an extra step or a few most of the time, but that's not the only option.
If you are working in a mathbox, then I'd say go ahead and put in your mathbox whatever theorems make sense to you. Either the theorems will get moved out of the mathbox in due course, or something else will happen to make another solution seem better.
Hope none of this is keeping you from getting those homeomorphic theorems proved!
-- 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/1fd9f879-0032-9af6-6407-edd74f4728b8%40panix.com.
