fnconstg

[tbrend...@gmail.com]

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.

[Thierry Arnoux]

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, tbrend...@gmail.com 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cd6c5c92-0f64-47db-9600-920b2b37f64bn%40googlegroups.com.

[Jim Kingdon]

> 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!

[Alexander van der Vekens]

According to our conventions (see section "Conventions" in set.mm):

       "Deduction form" is the preferred form for theorems because this form
       allows us to easily use the theorem in places where (in traditional
       textbook formalizations) the standard Deduction Theorem (see below)
       would be used. We call this approach <b>"deduction style"</b>.
       In contrast, we usually avoid theorems in "inference form" when that
       would end up requiring us to use the deduction theorem.

So adding ~fnconstd should be no problem, but adding ~fnconst ("inference form", like ~fconst) should be avoided.

As said already before, such a theorem should be usually added to a mathbox first.