> 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.
