Yes. That. On Sat, Nov 23, 2019 at 4:50 AM Thierry Arnoux <[email protected]> wrote:
> 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]. > 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 > <https://groups.google.com/d/msgid/metamath/912d97ea-6bd8-403a-7ec8-54434ac1d44f%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/CAFXXJSvrE%2Bt%2Bzn634MsDfVaPXBu514Ep_%3DPSk-9WAyDC-JUQdA%40mail.gmail.com.
