I'm a bit skeptical.
I remember Norm wrote a message to the mailing list (which I'm not sure
how to find) about why we use e. and C_ for ordinal less than and
ordinal no greater than, rather than having, say, <o and <_o (I think he
even said we tried the latter for a while). I don't know if there was a
similar discussion of 0o and (/).
If applying definitions in metamath were more automatic, maybe I would
feel differently (or maybe I wouldn't, I'm not sure), but as it is,
there would be a number of extra theorems (0o e. _V, 0o e. _om, 0o e.
1o, etc) and steps converting between 0o and (/).
On 7/21/22 13:13, 'Alexander van der Vekens' via Metamath wrote:
I want to suggest to provide a special symbol ` 0o `for the ordinal
number 0, which actually is the empty set `(/) `, see ~0elon and
df-1o. It would be just a synonym for ` (/) `:
` df-0o $a |- 0o = (/) $. `
With such a symbol, the theorems in the context of ordinal numbers can
be written in a more intuitive way. For example
` map0e $p |- ( A e. V -> ( A ^m (/) ) = 1o )`
could be written as
map0e $p |- ( A e. V -> ( A ^m 0o ) = 1o )
Was this already proposed/discussed before? What do others think about it?
--
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/c6bc77ee-56cd-458c-a176-3f616e0c862an%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/c6bc77ee-56cd-458c-a176-3f616e0c862an%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/7a3412de-8d5f-c3a1-2580-81e9cc8af336%40panix.com.
