Re: [isabelle] Inclusion-minimal sets

Hi Manuel,

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

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.



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