Dear fellow Metamathers, I think I've got it: I'll define "TarskiGLD <http://us2.metamath.org/mpeuni/df-trkgld.html>" as a relation, where ` G TarskiGLD N ` holds whenever ` G ` is a Tarskian geometry of dimension ` N ` or more. This does the trick without introducing any new syntax.
Sorry for answering so quickly, and to my own post! _ Thierry On 23/11/2019 17:33, Thierry Arnoux wrote:
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] <mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b0f0074a-00ad-15aa-dda7-cccb5d1fe98b%40gmx.net <https://groups.google.com/d/msgid/metamath/b0f0074a-00ad-15aa-dda7-cccb5d1fe98b%40gmx.net?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/912d97ea-6bd8-403a-7ec8-54434ac1d44f%40gmx.net.
