Tarski Geometries of dimension N or more
Thierry Arnoux
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" covers).
However I'm a bit stuck with "TarskiGLD",
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 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
Thierry Arnoux
Dear fellow Metamathers,
I think I've got it: I'll define "TarskiGLD"
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
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b0f0074a-00ad-15aa-dda7-cccb5d1fe98b%40gmx.net.
Mario Carneiro
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/912d97ea-6bd8-403a-7ec8-54434ac1d44f%40gmx.net.
Alexander van der Vekens
On Saturday, November 23, 2019 at 10:50:29 AM UTC+1, Thierry Arnoux wrote:
Dear fellow Metamathers,
I think I've got it: I'll define "TarskiGLD" 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" covers).
However I'm a bit stuck with "TarskiGLD", 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 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 meta...@googlegroups.com.