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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3dd47cc0-64c1-4ec8-aeb2-31fbd99482fc%40googlegroups.com.
