[isabelle] Inclusion-minimal sets


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?



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