[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
This archive was generated by a fusion of
Pipermail (Mailman edition) and