Many theorems are stated in several forms, including the deduction form, so an "fnconstd" would not be anything surprising, as you point out.
You can always first put the new theorem in your mathbox. Pretty quickly someone will either want to use it in his/her mathbox, or find out this can lead to relevant proof shortening, and move it to main. Good luck with "cmpcvxhmph" ! On 23/09/2023 02: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. -- 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/cd6c5c92-0f64-47db-9600-920b2b37f64bn%40googlegroups.com <https://groups.google.com/d/msgid/metamath/cd6c5c92-0f64-47db-9600-920b2b37f64bn%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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/90a94897-9bf4-d271-eefb-ab3a3d57b674%40gmx.net.
