Indeed this is a good opportunity to raise (again) the question about
the definition of odd integers.
I agree with Norm that` 2 || N ` is just as long as ` N e. Even `, and
therefore will not bring any database size improvement. Since it also
implies ` 2 e. ZZ `, I don't see worth in defining `Even`.
For `Odd` this does not hold, one cannot just replace it with ` -. 2 ||
N ` but also has to add ` N e. ZZ ` to recover a definition of `Odd`.
To circumvent this, I have been using essential hypotheses in the form
of ` O = { z e. ZZ | -. 2 || z } `, like in ~ hgt749d
<http://metamath.tirix.org:3030/mpests/hgt749d> and ~ eulerpart
<http://metamath.tirix.org:3030/mpests/eulerpart.j>.
This allows me to use the local `O` in the proof just like if it were a
definition. We could also use this trick in main without defining a new
symbol.
Anyway, I'd also like to point out that technically, nothing prevents
Alexander (sorry for the mix-up in my previous mail) to use theorems
from my Mathbox; this rule is nowhere enforced. Maybe a short comment
that this goes against the usage and why we chose to make an exception
would also work!
BR,
_
Thierry
On 14/01/2022 04:01, Jim Kingdon wrote:
I've tried to write up the situation about Even and Odd at
https://github.com/metamath/set.mm/issues/2433 . Hopefully it is
helpful for me to summarize what was a rather long thread the last
time this came up.
Hopefully we can find a solution - it would be kind of silly if
figuring out how to say "x is odd" prevents us from getting things out
of mathboxes which we otherwise would like to.
On 1/13/22 8:14 AM, 'Alexander van der Vekens' via Metamath wrote:
According to our rules, I cannot use ~tgoldbachgt in my Mathbox as
long as it is in Thierry`s mathbox! Maybe we can move the whole
material from both mathboxes to main set.mm? One difficulty would be,
however, that I intensivly use the classes Even and Odd (defined in
my mathbox), which were not allowed to be moved to main set.mm yet
(see github issue #1682).
--
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/89f8ac1a-6aa3-a643-24cf-81e43361a191%40gmx.net.
