On 14/05/2016 23:18, Manuel Eberl wrote:
Thanks, that worked great. I was a bit puzzled about why there is no lemma that states that theâ âproper subsetâ relation on finite sets is well-founded. I'll add that to the library. It would be nice to generalise the Min/Max operators to also work with non-linear orders.
I assume on weaker structures it would return some maximal element? I have no objection in principle, but they way Max is defined would have to be reorganized considerably and you should talk to Florian about that.
ArgMin/ArgMax would also be really useful.
I don't see this as core math material but as something for the library. Tobias
Any opinions on that? Cheers, Manuel
Description: S/MIME Cryptographic Signature