I wonder why (/) is/must be excluded from an extensible structure to be a
function:
df-struct $a |- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\
Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) } $.
Why Fun ( f \ { (/) } ) and not simply Fun f ?
I searched for a justification in set.mm and also in the google group, but
I did not find any hint. Formerly, there wasn't such a restriction, see
https://groups.google.com/g/metamath/c/BFFSR3b5qEo/m/s6vph-zL_DoJ.
Can anybody explain this restriction? Is there any meaningful structure
which contains the empty set, e .g. S = { (/) , <. ( Base ` ndx ) , B >. ,
<. ( E ` ndx ) , .+ >. } (will Fun S not hold in this case?)?
--
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/8213c12b-c060-4d15-b1d7-62a58536b724n%40googlegroups.com.
