I want to add that df-struct is essentially a technical definition made so as to make efficient (linear time) the proofs of n-ary versions of strle3. It is not meant to stake any claim on what a structure "is", and for various reasons you might want to add or remove hypotheses relative to df-struct. The main utility of this particular definition is that you can prove component extraction theorems easily, as long as all the components are written in increasing numerical order.
Historically, the definition of a structure is simply any set; we simply apply (Base`G) and (+g`G) and so on and use what we get without regard to how those operations are computed from G, whether it is a function or anything else. df-struct does not change this; it is a tool meant to help prove the component extraction theorems for particular structures given as finite sets of ordered pairs, and it is not a supertype of every structure - df-mgm does not mention it and is still defined with respect to all sets. On Mon, Nov 15, 2021 at 10:40 AM David A. Wheeler <[email protected]> wrote: > > > > On Nov 15, 2021, at 9:49 AM, 'Alexander van der Vekens' via Metamath < > [email protected]> wrote: > > > > Thank you, Mario, for your explanation. It sounds reasonable, although > it is more difficult to proof certain theorems for arbitrary extensible > structures: Since we cannot assume Fun S if S struct X (only Fun ( S \ { > (/) } ), see ~ structn0fun, or equivalently Fun `' `' S, see ~ > structfung), special versions of theorems with antecedent Fun F are needed > (see, for example, ~fundmge2nop0 vs. ~fundmge2nop). > > > > I plan to add this explanation to the comment within set.mm, so that it > is documented for everybody and for the future. > > Excellent! I love to see documentation on *why* things are done, > thanks for offering to do that. > > If you could, please include links to examples (e.g., ~ strle1 ). > The more hyperlinks there are between various entries, the easier > It is to see their interrelationships. I also think it’s fun to start in > one > place and in a few links discover relationships you hadn’t anticipated. > > --- David A. Wheeler > > -- > 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/379C3F57-E834-4B7B-9A38-102548E73743%40dwheeler.com > . > -- 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/CAFXXJSt-kt7YU2fPs-29han_y4XQMxMvwSjaqDm0EykOjNsK0g%40mail.gmail.com.
