Most of the definitions don't need to be moved up, only the "structural" ones that are required for actually defining the content of the new slot. df-gsum is unfortunate because it is a relatively complex definition that is also a dependency for the slot, but if you can write the slot without any auxiliaries then nothing has to move. (Another option is to unfold the definition in the content of df-prds, and then refold the definition when proving the slot theorem. But this would make df-prds even larger than it already is.)
Mario On Thu, Feb 13, 2020 at 12:53 PM Benoit <benoit.ju...@gmail.com> wrote: > On Thursday, February 13, 2020 at 5:46:36 PM UTC+1, Mario Carneiro wrote: >> >> That said, I think it would still be better to move all definitions >> needed for df-prds before it. This is a downside of the "everything >> structure" approach, but it does not displace too many definitions. We can >> keep the real theorems about them (including the definitional theorem) in >> their proper place. >> > > So it looks like my reply there ( > https://github.com/metamath/set.mm/issues/1457#issuecomment-585716367) > was unfortunately correct ? What happens to df-prds (and also image > structure, structure restriction, etc.) when we define new slots, for a > sigma-algebra, a measure, a smooth atlas, a structure sheaf, etc. ? > > Benoît > > -- > 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+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/3dd47cc0-64c1-4ec8-aeb2-31fbd99482fc%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/3dd47cc0-64c1-4ec8-aeb2-31fbd99482fc%40googlegroups.com?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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStBJg4qAEZB1dx%2BfDM3byK3C719Lh8w6nf0K1DkzgOUWw%40mail.gmail.com.
