As far as I interpret the comments until now, there is the tendeny towards not defining 0o, and generally avoid new definitions. This corresponds to our convention "New definitions infrequent.`" (although there can always be exceptions if they are reasonable and broadly accepted).
Just for the record: I also thought about a definition of "not defined" as ` df-ndef $a |- N/D = (/) $. ` to distinguish between the meaning of `(/) ` as " not defined" and "defined result". ~fvprc, for example, could become ` $p |- ( -. A e. _V -> ( F ` A ) = N/D ) $= `. Alternatively, N/D could be defined as predicate for classes: `df-ndef $a |- ( N/D A <-> A = (/) ) $. ( ~fvprc could become ` $p |- ( -. A e. _V -> N/D ( F ` A ) ) $= . -- 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/350afa44-5bb4-4597-9cc5-9b5a5459fa54n%40googlegroups.com.
