Dear fellow Metamathers, When introducing new concepts in Metamath, as a convention, I always try to define new /classes/, which are then either class builders, functions or operations, instead of introducing a new syntax notation (BTW, where is this "convention" written down? I think this is not exactly what the "/new definitions infrequent/ <http://us2.metamath.org/mpeuni/conventions.html>" covers).
However I'm a bit stuck with "TarskiGLD <http://us2.metamath.org/mpeuni/df-trkgld.html>", the Tarski geometries of dimension N or more. I initially wanted them defined as a function of N, however I believe the resulting set is a proper class, not allowing me to define it as a map-to function. Is there any trick I can use there? I thought about restricting to structures, like ` TarskiGLD = ( N e. NN |-> { g e. dom Struct | ... } ) ` , but dom Struct is also a proper class. Right now, my latest pull request <https://github.com/metamath/set.mm/pull/1266/files> has a new syntax notation "TarskiGLD ( N )" for that concept, but I would be interested in any suggestion! Thanks in advance for your insight! _ Thierry -- 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/b0f0074a-00ad-15aa-dda7-cccb5d1fe98b%40gmx.net.
