Email Gateway (Aug 22 2022 at 13:21): Email Gateway (Aug 22 2022 at 13:21):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I am looking for a way to obtain an inclusion-minimal set with a certain
property, i.e. I have a non-empty set of sets and I now want a set from
this set that is miminal w.r.t. set inclusion.
Since the union of my set of sets is finite, such an inclusion-minimal
set always exists.
Is there some easy way to do this with the set/lattice theory we already
have or do I have to construct this myself using Hilbert choice and
induction?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 13:22):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Manuel,
I have the impression you could use strict subset inclusion restricted to the finite set of sets as the relation in the lemmas in "finite_acyclic_wf" and "wf_eq_minimal" from "Wellfounded" and get what you want.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 13:22):From: Manuel Eberl <eberlm@in.tum.de>
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?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 13:22):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:22):From: Manuel Eberl <eberlm@in.tum.de>
I assume on weaker structures it would return some maximal element?
Yes. Perhaps this should then be separate from the "normal" Min/Max,
since one would not be able to generate code for Min/Max on non-linear
orders due to the non-unique nature of the definition.
Another perhaps less problematic way would be to define the set of /all/
maximal elements w.r.t. an order (perhaps even an order specified as a
predicate, not a typeclass) I already have something like this in my
formalisation of Social Choice Theory anyway.
Getting /some/ maximal element is then trivial and one has separated the
arbitrary choice from the maximality-related stuff.
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.
I guess I'll put it on my queue then.
Manuel
Last updated: Apr 27 2024 at 01:05 UTC