Re: [isabelle] Inclusion-minimal sets

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. ArgMin/ArgMax would also be really useful.

Any opinions on that?



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