Re: [isabelle] Inclusion-minimal sets

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.


Any opinions on that?



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.